src/HOL/TPTP/sledgehammer_tactics.ML
changeset 59498 50b60f501b05
parent 58928 23d0ffd48006
child 62738 fe827c6fa8c5
--- 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;