clarified Skip_Proof.cheat_tac: more standard tactic;
clarified Method.cheating: check quick_and_dirty when it is actually applied;

--- 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 =

--- a/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Mar 27 14:19:18 2013 +0100
+++ b/src/HOL/TPTP/sledgehammer_tactics.ML	Wed Mar 27 14:50:30 2013 +0100
@@ -64,12 +64,11 @@
 
 fun sledgehammer_as_oracle_tac ctxt override_params fact_override i th =
   let
-    val thy = Proof_Context.theory_of ctxt
     val override_params =
       override_params @
       [("preplay_timeout", "0"),
        ("minimize", "false")]
     val xs = run_prover override_params fact_override i i ctxt th
-  in if is_some xs then Skip_Proof.cheat_tac thy th else Seq.empty end
+  in if is_some xs then ALLGOALS Skip_Proof.cheat_tac th else Seq.empty end
 
 end;

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 27 14:19:18 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_aux.ML	Wed Mar 27 14:50:30 2013 +0100
@@ -1180,7 +1180,7 @@
 fun define_quickcheck_predicate t thy =
   let
     val (vs, t') = strip_abs t
-    val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs
+    val vs' = Variable.variant_frees (Proof_Context.init_global thy) [] vs (* FIXME proper context!? *)
     val t'' = subst_bounds (map Free (rev vs'), t')
     val (prems, concl) = strip_horn t''
     val constname = "quickcheck"
@@ -1191,8 +1191,9 @@
     val t = Logic.list_implies
       (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
        HOLogic.mk_Trueprop (list_comb (const, map Free vs')))
-    val tac = fn _ => Skip_Proof.cheat_tac thy1
-    val intro = Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t tac
+    val intro =
+      Goal.prove (Proof_Context.init_global thy1) (map fst vs') [] t
+        (fn _ => ALLGOALS Skip_Proof.cheat_tac)
   in
     ((((full_constname, constT), vs'), intro), thy1)
   end

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Mar 27 14:19:18 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML	Wed Mar 27 14:50:30 2013 +0100
@@ -134,7 +134,7 @@
   
 fun split_all_pairs thy th =
   let
-    val ctxt = Proof_Context.init_global thy
+    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     val ((_, [th']), _) = Variable.import true [th] ctxt
     val t = prop_of th'
     val frees = Term.add_frees t [] 
@@ -148,8 +148,9 @@
       in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
     val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
     val t' = Pattern.rewrite_term thy rewr [] t
-    val tac = Skip_Proof.cheat_tac thy
-    val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn _ => tac)
+    val th'' =
+      Goal.prove ctxt (Term.add_free_names t' []) [] t'
+        (fn _ => ALLGOALS Skip_Proof.cheat_tac)
     val th''' = Local_Defs.unfold ctxt [@{thm split_conv}, @{thm fst_conv}, @{thm snd_conv}] th''
   in
     th'''

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Mar 27 14:19:18 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_pred.ML	Wed Mar 27 14:50:30 2013 +0100
@@ -127,13 +127,13 @@
 
 fun flatten_intros constname intros thy =
   let
-    val ctxt = Proof_Context.init_global thy
+    val ctxt = Proof_Context.init_global thy  (* FIXME proper context!? *)
     val ((_, intros), ctxt') = Variable.import true intros ctxt
     val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
       (flatten constname) (map prop_of intros) ([], thy)
     val ctxt'' = Proof_Context.transfer thy' ctxt'
-    val tac = fn _ => Skip_Proof.cheat_tac thy'
-    val intros'' = map (fn t => Goal.prove ctxt'' [] [] t tac) intros'
+    val intros'' =
+      map (fn t => Goal.prove ctxt'' [] [] t (fn _ => ALLGOALS Skip_Proof.cheat_tac)) intros'
       |> Variable.export ctxt'' ctxt
   in
     (intros'', (local_defs, thy'))

--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Mar 27 14:19:18 2013 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_proof.ML	Wed Mar 27 14:50:30 2013 +0100
@@ -491,7 +491,7 @@
 
 fun prove_pred options thy clauses preds pred (_, mode) (moded_clauses, compiled_term) =
   let
-    val ctxt = Proof_Context.init_global thy
+    val ctxt = Proof_Context.init_global thy   (* FIXME proper context!? *)
     val clauses = case AList.lookup (op =) clauses pred of SOME rs => rs | NONE => []
   in
     Goal.prove ctxt (Term.add_free_names compiled_term []) [] compiled_term
@@ -503,7 +503,7 @@
         THEN print_tac options "proved one direction"
         THEN prove_other_direction options ctxt pred mode moded_clauses
         THEN print_tac options "proved other direction")
-      else (fn _ => Skip_Proof.cheat_tac thy))
+      else (fn _ => ALLGOALS Skip_Proof.cheat_tac))
   end;
 
 end;
\ No newline at end of file

--- a/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Mar 27 14:19:18 2013 +0100
+++ b/src/HOL/Tools/Quickcheck/quickcheck_common.ML	Wed Mar 27 14:50:30 2013 +0100
@@ -376,7 +376,7 @@
       let
         val eqs_t = mk_equations consts
         val eqs = map (fn eq => Goal.prove lthy argnames [] eq
-          (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of lthy))) eqs_t
+          (fn _ => ALLGOALS Skip_Proof.cheat_tac)) eqs_t
       in
         fold (fn (name, eq) => Local_Theory.note
           ((Binding.qualify true prfx

--- a/src/Pure/Isar/method.ML	Wed Mar 27 14:19:18 2013 +0100
+++ b/src/Pure/Isar/method.ML	Wed Mar 27 14:50:30 2013 +0100
@@ -20,7 +20,7 @@
   val SIMPLE_METHOD: tactic -> method
   val SIMPLE_METHOD': (int -> tactic) -> method
   val SIMPLE_METHOD'': ((int -> tactic) -> tactic) -> (int -> tactic) -> method
-  val cheating: bool -> Proof.context -> method
+  val cheating: bool -> method
   val intro: thm list -> method
   val elim: thm list -> method
   val unfold: thm list -> Proof.context -> method
@@ -112,7 +112,7 @@
 
 in
 
-fun insert_tac [] i = all_tac
+fun insert_tac [] _ = all_tac
   | insert_tac facts i = EVERY (map (fn th => cut_rule_tac th i) facts);
 
 val insert_facts = METHOD (ALLGOALS o insert_tac);
@@ -127,10 +127,10 @@
 
 (* cheating *)
 
-fun cheating int ctxt =
+fun cheating int = METHOD (fn _ => fn st =>
   if int orelse ! quick_and_dirty then
-    METHOD (K (Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt)))
-  else error "Cheating requires quick_and_dirty mode!";
+    ALLGOALS Skip_Proof.cheat_tac st
+  else error "Cheating requires quick_and_dirty mode!");
 
 
 (* unfold intro/elim rules *)
@@ -296,7 +296,7 @@
 val default_text = Source (Args.src (("default", []), Position.none));
 val this_text = Basic (K this);
 val done_text = Basic (K (SIMPLE_METHOD all_tac));
-fun sorry_text int = Basic (cheating int);
+fun sorry_text int = Basic (K (cheating int));
 
 fun finish_text (NONE, immed) = Basic (finish immed)
   | finish_text (SOME txt, immed) = Then [txt, Basic (finish immed)];

--- a/src/Pure/goal.ML	Wed Mar 27 14:19:18 2013 +0100
+++ b/src/Pure/goal.ML	Wed Mar 27 14:50:30 2013 +0100
@@ -324,7 +324,7 @@
 
 fun prove_sorry ctxt xs asms prop tac =
   if ! quick_and_dirty then
-    prove ctxt xs asms prop (fn _ => Skip_Proof.cheat_tac (Proof_Context.theory_of ctxt))
+    prove ctxt xs asms prop (fn _ => ALLGOALS Skip_Proof.cheat_tac)
   else (if future_enabled () then prove_future else prove) ctxt xs asms prop tac;
 
 fun prove_sorry_global thy xs asms prop tac =

--- a/src/Pure/skip_proof.ML	Wed Mar 27 14:19:18 2013 +0100
+++ b/src/Pure/skip_proof.ML	Wed Mar 27 14:50:30 2013 +0100
@@ -9,7 +9,7 @@
   val report: Proof.context -> unit
   val make_thm_cterm: cterm -> thm
   val make_thm: theory -> term -> thm
-  val cheat_tac: theory -> tactic
+  val cheat_tac: int -> tactic
 end;
 
 structure Skip_Proof: SKIP_PROOF =
@@ -32,7 +32,7 @@
 
 (* cheat_tac *)
 
-fun cheat_tac thy st =
-  ALLGOALS (rtac (make_thm thy (Var (("A", 0), propT)))) st;
+fun cheat_tac i st =
+  rtac (make_thm (Thm.theory_of_thm st) (Var (("A", 0), propT))) i st;
 
 end;