src/Tools/solve_direct.ML

--- a/src/Tools/solve_direct.ML	Wed Mar 27 17:55:21 2013 +0100
+++ b/src/Tools/solve_direct.ML	Wed Mar 27 17:58:07 2013 +0100
@@ -109,7 +109,8 @@
 val _ =
   Outer_Syntax.improper_command @{command_spec "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.unknown_proof o
+      Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
 
 
 (* hook *)