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/Tools/SMT/z3_proof_parser.ML
changeset 46497 89ccf66aa73d
parent 44718 b656af4c9796 
--- a/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/SMT/z3_proof_parser.ML	Wed Feb 15 23:19:30 2012 +0100
@@ -134,7 +134,7 @@
         | _ => SMT_Utils.certify ctxt (Var ((Name.uu, maxidx_of ct + 1), T)))
       fun dec (i, v) = if i = 0 then NONE else SOME (i-1, v)
       val vars' = map_filter dec vars
-    in (Thm.capply (SMT_Utils.instT' cv q) (Thm.cabs cv ct), vars') end
+    in (Thm.apply (SMT_Utils.instT' cv q) (Thm.lambda cv ct), vars') end
 
   fun quant name =
     SMT_Utils.mk_const_pat @{theory} name (SMT_Utils.destT1 o SMT_Utils.destT1)
isabelle