--- 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 *)