diff -r 0c5cd369a643 -r 50b60f501b05 src/HOL/TPTP/sledgehammer_tactics.ML --- a/src/HOL/TPTP/sledgehammer_tactics.ML Tue Feb 10 14:29:36 2015 +0100 +++ b/src/HOL/TPTP/sledgehammer_tactics.ML Tue Feb 10 14:48:26 2015 +0100 @@ -70,7 +70,7 @@ ("minimize", "false")] val xs = run_prover override_params fact_override chained i i ctxt th in - if is_some xs then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty + if is_some xs then ALLGOALS (Skip_Proof.cheat_tac ctxt) th else Seq.empty end end;