--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Nov 03 14:31:15 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Nov 03 14:50:27 2014 +0100
@@ -386,7 +386,7 @@
no_fact_override
val _ =
- Outer_Syntax.improper_command @{command_spec "sledgehammer"}
+ Outer_Syntax.command @{command_spec "sledgehammer"}
"search for first-order proof using automatic theorem provers"
((Scan.optional Parse.name runN -- parse_params
-- parse_fact_override -- Scan.option Parse.nat) #>> sledgehammer_trans)