--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu May 15 18:18:50 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML Thu May 15 20:48:13 2014 +0200
@@ -358,8 +358,9 @@
val default_learn_prover_timeout = 2.0
-fun hammer_away override_params subcommand opt_i fact_override state =
+fun hammer_away override_params subcommand opt_i fact_override state0 =
let
+ val state = Proof.map_context (Try0.silence_methods false) state0
val thy = Proof.theory_of state
val ctxt = Proof.context_of state