src/Tools/solve_direct.ML

--- a/src/Tools/solve_direct.ML	Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Tools/solve_direct.ML	Thu Apr 16 14:18:32 2015 +0200
@@ -94,8 +94,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword solve_direct}
     "try to solve conjectures directly with existing theorems"
-    (Scan.succeed (Toplevel.unknown_proof o
-      Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
+    (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
 
 
 (* hook *)