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/smt_solver.ML
changeset 41131 fc9d503c3d67
parent 41127 2ea84c8535c6
child 41239 d6e804ff29c3 
--- a/src/HOL/Tools/SMT/smt_solver.ML	Wed Dec 15 10:12:48 2010 +0100
+++ b/src/HOL/Tools/SMT/smt_solver.ML	Wed Dec 15 10:12:48 2010 +0100
@@ -220,8 +220,8 @@
     SMT_Normalize.normalize ctxt iwthms
     |> rpair ctxt
     |-> SMT_Monomorph.monomorph
-    |-> invoke name cmd options
-    |> reconstruct ctxt
+    |> (fn (iwthms', ctxt') => invoke name cmd options iwthms' ctxt'
+    |> reconstruct ctxt')
     |> (fn (idxs, thm) => thm
     |> tap (fn _ => trace_assumptions ctxt iwthms idxs)
     |> pair idxs)
isabelle