diff -r ea1d9408a233 -r 29ec8680e61f src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Feb 13 13:16:16 2014 +0100 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Thu Feb 13 13:16:17 2014 +0100 @@ -353,8 +353,8 @@ (used_facts, Lazy.lazy (fn () => let val used_pairs = used_from |> filter_used_facts false used_facts in - play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal (hd meths) - meths + play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal + (hd meths) meths end), fn preplay => let