--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jun 29 19:27:07 2015 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Mon Jun 29 20:55:46 2015 +0200
@@ -408,7 +408,7 @@
val _ = Try.tool_setup (sledgehammerN, (40, @{system_option auto_sledgehammer}, try_sledgehammer))
val _ =
- Query_Operation.register sledgehammerN (fn {state = st, args, output_result} =>
+ Query_Operation.register {name = sledgehammerN, pri = 0} (fn {state = st, args, output_result} =>
(case try Toplevel.proof_of st of
SOME state =>
let