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/Tools/solve_direct.ML
changeset 60190 906de96ba68a
parent 60094 96a4765ba7d1
child 63728 4e078ae3682c 
--- a/src/Tools/solve_direct.ML	Wed Apr 22 19:48:32 2015 +0200
+++ b/src/Tools/solve_direct.ML	Wed Apr 22 20:14:43 2015 +0200
@@ -94,7 +94,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword solve_direct}
     "try to solve conjectures directly with existing theorems"
-    (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
+    (Scan.succeed (Toplevel.keep_proof (ignore o solve_direct o Toplevel.proof_of)));
 
 
 (* hook *)
isabelle