--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Dec 03 08:40:47 2010 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Dec 03 09:55:45 2010 +0100
@@ -347,14 +347,11 @@
parse_sledgehammer_params_command
fun auto_sledgehammer state =
- if not (!auto) then
- (false, state)
- else
- let val ctxt = Proof.context_of state in
- run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
- (minimize_command [] 1) state
- end
+ let val ctxt = Proof.context_of state in
+ run_sledgehammer (get_params true ctxt []) true 1 no_relevance_override
+ (minimize_command [] 1) state
+ end
-val setup = Auto_Tools.register_tool (sledgehammerN, auto_sledgehammer)
+val setup = Auto_Tools.register_tool (auto, auto_sledgehammer)
end;