Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Library/Old_SMT/old_z3_proof_parser.ML
changeset 60642 48dd1cefb4ae
parent 59634 4b94cc030ba0 
--- a/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Fri Jul 03 16:19:45 2015 +0200
+++ b/src/HOL/Library/Old_SMT/old_z3_proof_parser.ML	Sun Jul 05 15:02:30 2015 +0200
@@ -109,7 +109,7 @@
     val max = fold (Integer.max o fst) vars 0
     val ns = fst (Variable.variant_fixes (replicate (max + 1) var_prefix) ctxt)
     fun mk (i, v) =
-      (v, Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
+      (dest_Var (Thm.term_of v), Thm.cterm_of ctxt (Free (nth ns i, Thm.typ_of_cterm v)))
   in map mk vars end
 
 fun close ctxt (ct, vars) =
@@ -161,7 +161,10 @@
         if null vars then ([], vars)
         else fold part vars ([], [])
 
-    in (Thm.instantiate_cterm ([], inst) ct, (maxidx', vars' @ all_vars)) end
+    in
+      (Thm.instantiate_cterm ([], map (apfst (dest_Var o Thm.term_of)) inst) ct,
+        (maxidx', vars' @ all_vars))
+    end
 in
 fun mk_fun f ts =
   let val (cts, (_, vars)) = fold_map prep ts (0, [])
isabelle