diff -r 343905de27b1 -r b8ffc3dc9e24 src/Tools/solve_direct.ML
--- a/src/Tools/solve_direct.ML	Mon Apr 06 16:30:44 2015 +0200
+++ b/src/Tools/solve_direct.ML	Mon Apr 06 17:06:48 2015 +0200
@@ -92,7 +92,7 @@
 val solve_direct = do_solve_direct Normal
 
 val _ =
-  Outer_Syntax.command @{command_spec "solve_direct"}
+  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)));