# HG changeset patch
# User wenzelm
# Date 1255791483 -7200
# Node ID fbd2bb2489a84bd200025d48dbdc5c169e6b4b69
# Parent  15489e162b21250d5621958496c7a863ba3575fd
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;

diff -r 15489e162b21 -r fbd2bb2489a8 NEWS
--- a/NEWS	Sat Oct 17 16:40:41 2009 +0200
+++ b/NEWS	Sat Oct 17 16:58:03 2009 +0200
@@ -250,6 +250,9 @@
 Syntax.pretty_typ/term directly, preferably with proper context
 instead of global theory.
 
+* Operations of structure Skip_Proof (formerly SkipProof) no longer
+require quick_and_dirty mode, which avoids critical setmp.
+
 
 *** System ***
 
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Import/import.ML
--- a/src/HOL/Import/import.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Import/import.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -26,7 +26,7 @@
 
 fun import_tac ctxt (thyname, thmname) =
     if ! quick_and_dirty
-    then SkipProof.cheat_tac (ProofContext.theory_of ctxt)
+    then Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)
     else
      fn th =>
         let
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Import/replay.ML
--- a/src/HOL/Import/replay.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Import/replay.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -320,7 +320,7 @@
 
 fun replay_chached_thm int_thms thyname thmname =
     let
-        fun th_of thy = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
+        fun th_of thy = Skip_Proof.make_thm thy
         fun err msg = raise ERR "replay_cached_thm" msg
         val _ = writeln ("Replaying (from cache) "^thmname^" ...")
         fun rps [] thy = thy
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/Datatype/datatype_abs_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -69,7 +69,7 @@
           (split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
 
       in
-        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+        Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
           (fn {prems, ...} => EVERY
             [rtac induct' 1,
              REPEAT (rtac TrueI 1),
@@ -215,7 +215,7 @@
            (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
               THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs));
 
-      in split_conj_thm (SkipProof.prove_global thy1 [] []
+      in split_conj_thm (Skip_Proof.prove_global thy1 [] []
         (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
       end;
 
@@ -250,7 +250,7 @@
 
     val _ = message config "Proving characteristic theorems for primrec combinators ..."
 
-    val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
+    val rec_thms = map (fn t => Skip_Proof.prove_global thy2 [] [] t
       (fn _ => EVERY
         [rewrite_goals_tac reccomb_defs,
          rtac the1_equality 1,
@@ -330,7 +330,7 @@
           Library.take (length newTs, reccomb_names)) ([], thy1)
       ||> Theory.checkpoint;
 
-    val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
+    val case_thms = map (map (fn t => Skip_Proof.prove_global thy2 [] [] t
       (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
           (DatatypeProp.make_cases new_type_names descr sorts thy2)
   in
@@ -364,8 +364,8 @@
         val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
           (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))])
       in
-        (SkipProof.prove_global thy [] [] t1 tacf,
-         SkipProof.prove_global thy [] [] t2 tacf)
+        (Skip_Proof.prove_global thy [] [] t1 tacf,
+         Skip_Proof.prove_global thy [] [] t2 tacf)
       end;
 
     val split_thm_pairs = map prove_split_thms
@@ -384,7 +384,7 @@
 fun prove_weak_case_congs new_type_names descr sorts thy =
   let
     fun prove_weak_case_cong t =
-       SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+       Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
          (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1])
 
     val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
@@ -405,7 +405,7 @@
               hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
           | tac i n = rtac disjI2 i THEN tac i (n - 1)
       in 
-        SkipProof.prove_global thy [] [] t (fn _ =>
+        Skip_Proof.prove_global thy [] [] t (fn _ =>
           EVERY [rtac allI 1,
            exh_tac (K exhaustion) 1,
            ALLGOALS (fn i => tac i (i-1))])
@@ -427,7 +427,7 @@
         val [v] = Term.add_vars (concl_of nchotomy') [];
         val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy'
       in
-        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
+        Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
           (fn {prems, ...} => 
             let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
             in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/Datatype/datatype_codegen.ML
--- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -384,7 +384,7 @@
     val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
     val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss addsimps 
       (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
-    fun prove prop = SkipProof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
+    fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
       |> Simpdata.mk_eq;
   in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
 
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/Datatype/datatype_rep_proofs.ML
--- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -344,7 +344,7 @@
         (* prove characteristic equations *)
 
         val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
-        val char_thms' = map (fn eqn => SkipProof.prove_global thy' [] [] eqn
+        val char_thms' = map (fn eqn => Skip_Proof.prove_global thy' [] [] eqn
           (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
 
       in (thy', char_thms' @ char_thms) end;
@@ -366,7 +366,7 @@
             val Ts = map (TFree o rpair HOLogic.typeS)
               (Name.variant_list used (replicate i "'t"));
             val f = Free ("f", Ts ---> U)
-          in SkipProof.prove_global thy [] [] (Logic.mk_implies
+          in Skip_Proof.prove_global thy [] [] (Logic.mk_implies
             (HOLogic.mk_Trueprop (HOLogic.list_all
                (map (pair "x") Ts, S $ app_bnds f i)),
              HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
@@ -403,7 +403,7 @@
         val inj_thms' = map snd newT_iso_inj_thms @
           map (fn r => r RS @{thm injD}) inj_thms;
 
-        val inj_thm = SkipProof.prove_global thy5 [] []
+        val inj_thm = Skip_Proof.prove_global thy5 [] []
           (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
             [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
              REPEAT (EVERY
@@ -429,7 +429,7 @@
                              (split_conj_thm inj_thm);
 
         val elem_thm = 
-            SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
+            Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
               (fn _ =>
                EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
                 rewrite_goals_tac rewrites,
@@ -466,7 +466,7 @@
 
     val iso_thms = if length descr = 1 then [] else
       Library.drop (length newTs, split_conj_thm
-        (SkipProof.prove_global thy5 [] [] iso_t (fn _ => EVERY
+        (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
            [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
             REPEAT (rtac TrueI 1),
             rewrite_goals_tac (mk_meta_eq choice_eq ::
@@ -496,7 +496,7 @@
       let
         val inj_thms = map fst newT_iso_inj_thms;
         val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
-      in SkipProof.prove_global thy5 [] [] eqn (fn _ => EVERY
+      in Skip_Proof.prove_global thy5 [] [] eqn (fn _ => EVERY
         [resolve_tac inj_thms 1,
          rewrite_goals_tac rewrites,
          rtac refl 3,
@@ -520,7 +520,7 @@
         fun prove [] = []
           | prove (t :: ts) =
               let
-                val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
+                val dist_thm = Skip_Proof.prove_global thy5 [] [] t (fn _ =>
                   EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
               in dist_thm :: Drule.standard (dist_thm RS not_sym) :: prove ts end;
       in prove ts end;
@@ -535,7 +535,7 @@
         (iso_inj_thms @
           [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
            Lim_inject, Suml_inject, Sumr_inject]))
-      in SkipProof.prove_global thy5 [] [] t (fn _ => EVERY
+      in Skip_Proof.prove_global thy5 [] [] t (fn _ => EVERY
         [rtac iffI 1,
          REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
          dresolve_tac rep_congs 1, dtac box_equals 1,
@@ -585,7 +585,7 @@
 
     val cert = cterm_of thy6;
 
-    val indrule_lemma = SkipProof.prove_global thy6 [] []
+    val indrule_lemma = Skip_Proof.prove_global thy6 [] []
       (Logic.mk_implies
         (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
          HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
@@ -600,7 +600,7 @@
     val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
 
     val dt_induct_prop = DatatypeProp.make_ind descr sorts;
-    val dt_induct = SkipProof.prove_global thy6 []
+    val dt_induct = Skip_Proof.prove_global thy6 []
       (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
       (fn {prems, ...} => EVERY
         [rtac indrule_lemma' 1,
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/Function/size.ML
--- a/src/HOL/Tools/Function/size.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Function/size.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -164,7 +164,7 @@
 
     fun prove_unfolded_size_eqs size_ofp fs =
       if null recTs2 then []
-      else split_conj_thm (SkipProof.prove ctxt xs []
+      else split_conj_thm (Skip_Proof.prove ctxt xs []
         (HOLogic.mk_Trueprop (mk_conj (replicate l HOLogic.true_const @
            map (mk_unfolded_size_eq (AList.lookup op =
                (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
@@ -198,7 +198,7 @@
 
     fun prove_size_eqs p size_fns size_ofp simpset =
       maps (fn (((_, (_, _, constrs)), size_const), T) =>
-        map (fn constr => Drule.standard (SkipProof.prove ctxt [] []
+        map (fn constr => Drule.standard (Skip_Proof.prove ctxt [] []
           (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
              size_ofp size_const T constr)
           (fn _ => simp_tac simpset 1))) constrs)
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -108,7 +108,7 @@
       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 = setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy)
+    val tac = Skip_Proof.cheat_tac thy
     val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
     val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
   in
@@ -117,7 +117,7 @@
 
 fun normalize_equation thy th =
   mk_meta_equation th
-	|> Pred_Compile_Set.unfold_set_notation
+  |> Pred_Compile_Set.unfold_set_notation
   |> full_fun_cong_expand
   |> split_all_pairs thy
   |> tap check_equation_format
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -56,7 +56,7 @@
     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 tac = fn _ => setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy')
+    val tac = fn _ => Skip_Proof.cheat_tac thy'
     val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
       |> Variable.export ctxt' ctxt
   in
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML
--- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -58,7 +58,7 @@
     val t = Logic.list_implies
       (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
        HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
-    val tac = fn _ => setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy')
+    val tac = fn _ => Skip_Proof.cheat_tac thy'
     val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
     val _ = tracing (Display.string_of_thm ctxt' intro)
     val thy'' = thy'
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -661,7 +661,7 @@
     val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
     val nparams = guess_nparams T
     val pre_elim = 
-      (Drule.standard o (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)))
+      (Drule.standard o Skip_Proof.make_thm thy)
       (mk_casesrule (ProofContext.init thy) nparams pre_intros)
   in register_predicate (pre_intros, pre_elim, nparams) thy end
 
@@ -2082,7 +2082,7 @@
         THEN print_tac "proved one direction"
         THEN prove_other_direction thy modes pred mode moded_clauses
         THEN print_tac "proved other direction")
-      else (fn _ => setmp_CRITICAL quick_and_dirty true SkipProof.cheat_tac thy))
+      else fn _ => Skip_Proof.cheat_tac thy)
   end;
 
 (* composition of mode inference, definition, compilation and proof *)
@@ -2110,8 +2110,7 @@
     (join_preds_modes moded_clauses compiled_terms)
 
 fun prove_by_skip thy _ _ _ _ compiled_terms =
-  map_preds_modes (fn pred => fn mode => fn t =>
-      Drule.standard (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy) t))
+  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
     compiled_terms
     
 fun prepare_intrs thy prednames =
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/inductive.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -321,7 +321,7 @@
 fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
  (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
     "  Proving monotonicity ...";
-  (if skip_mono then SkipProof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
+  (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
     [] []
     (HOLogic.mk_Trueprop
       (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
@@ -350,7 +350,7 @@
     val rules = [refl, TrueI, notFalseI, exI, conjI];
 
     val intrs = map_index (fn (i, intr) => rulify
-      (SkipProof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY
+      (Skip_Proof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY
        [rewrite_goals_tac rec_preds_defs,
         rtac (unfold RS iffD2) 1,
         EVERY1 (select_disj (length intr_ts) (i + 1)),
@@ -395,7 +395,7 @@
         val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
            map mk_elim_prem (map #1 c_intrs)
       in
-        (SkipProof.prove ctxt'' [] prems P
+        (Skip_Proof.prove ctxt'' [] prems P
           (fn {prems, ...} => EVERY
             [cut_facts_tac [hd prems] 1,
              rewrite_goals_tac rec_preds_defs,
@@ -558,7 +558,7 @@
 
     val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
 
-    val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl
+    val induct = Skip_Proof.prove ctxt'' [] ind_prems ind_concl
       (fn {prems, ...} => EVERY
         [rewrite_goals_tac [inductive_conj_def],
          DETERM (rtac raw_fp_induct 1),
@@ -575,7 +575,7 @@
              (inductive_conj_def :: rec_preds_defs @ simp_thms'') prem,
            conjI, refl] 1)) prems)]);
 
-    val lemma = SkipProof.prove ctxt'' [] []
+    val lemma = Skip_Proof.prove ctxt'' [] []
       (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
         [rewrite_goals_tac rec_preds_defs,
          REPEAT (EVERY
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/quickcheck_generators.ML
--- a/src/HOL/Tools/quickcheck_generators.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -149,7 +149,7 @@
     val tac = ALLGOALS (rtac rule)
       THEN ALLGOALS (simp_tac rew_ss)
       THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)))
-    val simp = SkipProof.prove lthy' [v] [] eq (K tac);
+    val simp = Skip_Proof.prove lthy' [v] [] eq (K tac);
   in (simp, lthy') end;
 
 end;
@@ -185,7 +185,7 @@
               ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
               THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
               THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
-          in (map (fn prop => SkipProof.prove lthy [v] [] prop tac) eqs, lthy) end;
+          in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
       in
         lthy
         |> random_aux_primrec aux_eq'
@@ -206,7 +206,7 @@
       let
         val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
         val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
-      in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
+      in (map (fn prop => Skip_Proof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
     val b = Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"));
   in
     lthy
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/record.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -1040,7 +1040,7 @@
   if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty then
     Goal.prove (ProofContext.init thy) [] []
       (Logic.list_implies (map Logic.varify asms, Logic.varify prop))
-      (K (SkipProof.cheat_tac @{theory HOL}))
+      (K (Skip_Proof.cheat_tac @{theory HOL}))
       (*Drule.standard can take quite a while for large records, thats why
         we varify the proposition manually here.*)
   else
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/sat_funcs.ML
--- a/src/HOL/Tools/sat_funcs.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/sat_funcs.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -337,7 +337,7 @@
 		val _ = if !trace_sat then
 				tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
 			else ()
-		val False_thm = SkipProof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
+		val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
 	in
 		(* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
 		(* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/Tools/typedef.ML
--- a/src/HOL/Tools/typedef.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/Tools/typedef.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -199,8 +199,7 @@
 
     (*test theory errors now!*)
     val test_thy = Theory.copy thy;
-    val _ = test_thy
-      |> typedef_result (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm test_thy) goal);
+    val _ = typedef_result (Skip_Proof.make_thm test_thy goal) test_thy;
 
   in (set, goal, goal_pat, typedef_result) end
   handle ERROR msg =>
diff -r 15489e162b21 -r fbd2bb2489a8 src/HOL/ex/predicate_compile.ML
--- a/src/HOL/ex/predicate_compile.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/HOL/ex/predicate_compile.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -114,10 +114,10 @@
 val do_proofs = Unsynchronized.ref true;
 
 fun mycheat_tac thy i st =
-  (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
+  (Tactic.rtac (Skip_Proof.make_thm thy (Var (("A", 0), propT))) i) st
 
 fun remove_last_goal thy st =
-  (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
+  (Tactic.rtac (Skip_Proof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
 
 (* reference to preprocessing of InductiveSet package *)
 
@@ -1866,7 +1866,7 @@
     (join_preds_modes moded_clauses compiled_terms)
 
 fun prove_by_skip thy _ _ _ _ compiled_terms =
-  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (SkipProof.make_thm thy t))
+  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
     compiled_terms
     
 fun prepare_intrs thy prednames =
diff -r 15489e162b21 -r fbd2bb2489a8 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/Pure/Isar/class.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -76,7 +76,7 @@
         val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
         val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
         val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
-      in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
+      in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
     val assm_intro = Option.map prove_assm_intro
       (fst (Locale.intros_of thy class));
 
@@ -93,7 +93,7 @@
       (Tactic.match_tac (axclass_intro :: sup_of_classes
          @ loc_axiom_intros @ base_sort_trivs)
            ORELSE' Tactic.assume_tac));
-    val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
+    val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac);
 
   in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
 
diff -r 15489e162b21 -r fbd2bb2489a8 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/Pure/Isar/class_target.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -239,7 +239,7 @@
       [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
         (fst o rules thy) sub];
     val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
-    val classrel = SkipProof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
+    val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
       (K tac);
     val diff_sort = Sign.complete_sort thy [sup]
       |> subtract (op =) (Sign.complete_sort thy [sub])
diff -r 15489e162b21 -r fbd2bb2489a8 src/Pure/Isar/skip_proof.ML
--- a/src/Pure/Isar/skip_proof.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/Pure/Isar/skip_proof.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -1,7 +1,8 @@
 (*  Title:      Pure/Isar/skip_proof.ML
     Author:     Markus Wenzel, TU Muenchen
 
-Skipping proofs -- quick_and_dirty mode.
+Skipping proofs -- via oracle (in quick and dirty mode) or by forking
+(parallel mode).
 *)
 
 signature SKIP_PROOF =
@@ -14,15 +15,13 @@
     ({prems: thm list, context: Proof.context} -> tactic) -> thm
 end;
 
-structure SkipProof: SKIP_PROOF =
+structure Skip_Proof: SKIP_PROOF =
 struct
 
 (* oracle setup *)
 
 val (_, skip_proof) = Context.>>> (Context.map_theory_result
-  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) =>
-    if ! quick_and_dirty then Thm.cterm_of thy prop
-    else error "Proof may be skipped in quick_and_dirty mode only!")));
+  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) => Thm.cterm_of thy prop)));
 
 
 (* basic cheating *)
@@ -36,7 +35,7 @@
   (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
     (fn args => fn st =>
       if ! quick_and_dirty
-      then setmp_CRITICAL quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
+      then cheat_tac (ProofContext.theory_of ctxt) st
       else tac args st);
 
 fun prove_global thy xs asms prop tac =
diff -r 15489e162b21 -r fbd2bb2489a8 src/Pure/codegen.ML
--- a/src/Pure/codegen.ML	Sat Oct 17 16:40:41 2009 +0200
+++ b/src/Pure/codegen.ML	Sat Oct 17 16:58:03 2009 +0200
@@ -280,8 +280,7 @@
   let
     val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
     (* fake definition *)
-    val eq = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
-      (Logic.mk_equals (x, t));
+    val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
     fun err () = error "preprocess_term: bad preprocessor"
   in case map prop_of (preprocess thy [eq]) of
       [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()