--- a/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 23:20:12 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_prover_atp.ML Mon Feb 03 23:38:33 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 debug verbose preplay_timeout used_pairs state subgoal
- (hd meths) meths
+ play_one_line_proof mode verbose preplay_timeout used_pairs state subgoal (hd meths)
+ meths
end),
fn preplay =>
let