aboutsummaryrefslogtreecommitdiff
path: root/proofs/logic.ml
diff options
context:
space:
mode:
Diffstat (limited to 'proofs/logic.ml')
-rw-r--r--proofs/logic.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a92276cc83..db9b7c1107 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -157,7 +157,7 @@ let new_meta_variables =
| IsCast (c,t) -> mkCast (newrec c, t)
| IsAppL (f,cl) -> applist (newrec f, List.map newrec cl)
| IsMutCase (ci,p,c,lf) ->
- mkMutCaseA ci (newrec p) (newrec c) (Array.map newrec lf)
+ mkMutCase (ci, newrec p, newrec c, Array.map newrec lf)
| _ -> x
in
newrec