src/HOL/TPTP/atp_problem_import.ML

--- a/src/HOL/TPTP/atp_problem_import.ML	Wed Mar 27 14:19:18 2013 +0100
+++ b/src/HOL/TPTP/atp_problem_import.ML	Wed Mar 27 14:50:30 2013 +0100
@@ -175,7 +175,7 @@
         val (outcome, _) =
           Nitpick.pick_nits_in_term state params Nitpick.Normal i n step subst
                                     [] [] conj
-      in if outcome = "none" then Skip_Proof.cheat_tac thy th else Seq.empty end
+      in if outcome = "none" then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end
   end
 
 fun atp_tac ctxt completeness override_params timeout prover =