src/Tools/solve_direct.ML
changeset 46961 5c6955f487e5
parent 45666 d83797ef0d2d
child 49358 0fa351b1bd14
--- a/src/Tools/solve_direct.ML	Fri Mar 16 14:46:13 2012 +0100
+++ b/src/Tools/solve_direct.ML	Fri Mar 16 18:20:12 2012 +0100
@@ -107,10 +107,9 @@
 val solve_direct = do_solve_direct Normal
 
 val _ =
-  Outer_Syntax.improper_command solve_directN
-    "try to solve conjectures directly with existing theorems" Keyword.diag
-    (Scan.succeed
-      (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
+  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)));
 
 
 (* hook *)