operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
authorwenzelm
Sat Oct 17 16:58:03 2009 +0200 (2009-10-17 ago)
changeset 32970fbd2bb2489a8
parent 32969 15489e162b21
child 32971 55ba9b6648ef
operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
NEWS
src/HOL/Import/import.ML
src/HOL/Import/replay.ML
src/HOL/Tools/Datatype/datatype_abs_proofs.ML
src/HOL/Tools/Datatype/datatype_codegen.ML
src/HOL/Tools/Datatype/datatype_rep_proofs.ML
src/HOL/Tools/Function/size.ML
src/HOL/Tools/Predicate_Compile/pred_compile_data.ML
src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML
src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/quickcheck_generators.ML
src/HOL/Tools/record.ML
src/HOL/Tools/sat_funcs.ML
src/HOL/Tools/typedef.ML
src/HOL/ex/predicate_compile.ML
src/Pure/Isar/class.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/skip_proof.ML
src/Pure/codegen.ML
     1.1 --- a/NEWS	Sat Oct 17 16:40:41 2009 +0200
     1.2 +++ b/NEWS	Sat Oct 17 16:58:03 2009 +0200
     1.3 @@ -250,6 +250,9 @@
     1.4  Syntax.pretty_typ/term directly, preferably with proper context
     1.5  instead of global theory.
     1.6  
     1.7 +* Operations of structure Skip_Proof (formerly SkipProof) no longer
     1.8 +require quick_and_dirty mode, which avoids critical setmp.
     1.9 +
    1.10  
    1.11  *** System ***
    1.12  
     2.1 --- a/src/HOL/Import/import.ML	Sat Oct 17 16:40:41 2009 +0200
     2.2 +++ b/src/HOL/Import/import.ML	Sat Oct 17 16:58:03 2009 +0200
     2.3 @@ -26,7 +26,7 @@
     2.4  
     2.5  fun import_tac ctxt (thyname, thmname) =
     2.6      if ! quick_and_dirty
     2.7 -    then SkipProof.cheat_tac (ProofContext.theory_of ctxt)
     2.8 +    then Skip_Proof.cheat_tac (ProofContext.theory_of ctxt)
     2.9      else
    2.10       fn th =>
    2.11          let
     3.1 --- a/src/HOL/Import/replay.ML	Sat Oct 17 16:40:41 2009 +0200
     3.2 +++ b/src/HOL/Import/replay.ML	Sat Oct 17 16:58:03 2009 +0200
     3.3 @@ -320,7 +320,7 @@
     3.4  
     3.5  fun replay_chached_thm int_thms thyname thmname =
     3.6      let
     3.7 -        fun th_of thy = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
     3.8 +        fun th_of thy = Skip_Proof.make_thm thy
     3.9          fun err msg = raise ERR "replay_cached_thm" msg
    3.10          val _ = writeln ("Replaying (from cache) "^thmname^" ...")
    3.11          fun rps [] thy = thy
     4.1 --- a/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sat Oct 17 16:40:41 2009 +0200
     4.2 +++ b/src/HOL/Tools/Datatype/datatype_abs_proofs.ML	Sat Oct 17 16:58:03 2009 +0200
     4.3 @@ -69,7 +69,7 @@
     4.4            (split_conj_thm (cterm_instantiate insts' induct)) i) RSN (2, rev_mp))
     4.5  
     4.6        in
     4.7 -        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
     4.8 +        Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
     4.9            (fn {prems, ...} => EVERY
    4.10              [rtac induct' 1,
    4.11               REPEAT (rtac TrueI 1),
    4.12 @@ -215,7 +215,7 @@
    4.13             (((rtac induct' THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1
    4.14                THEN rewrite_goals_tac [mk_meta_eq choice_eq], rec_intrs));
    4.15  
    4.16 -      in split_conj_thm (SkipProof.prove_global thy1 [] []
    4.17 +      in split_conj_thm (Skip_Proof.prove_global thy1 [] []
    4.18          (HOLogic.mk_Trueprop (mk_conj rec_unique_ts)) (K tac))
    4.19        end;
    4.20  
    4.21 @@ -250,7 +250,7 @@
    4.22  
    4.23      val _ = message config "Proving characteristic theorems for primrec combinators ..."
    4.24  
    4.25 -    val rec_thms = map (fn t => SkipProof.prove_global thy2 [] [] t
    4.26 +    val rec_thms = map (fn t => Skip_Proof.prove_global thy2 [] [] t
    4.27        (fn _ => EVERY
    4.28          [rewrite_goals_tac reccomb_defs,
    4.29           rtac the1_equality 1,
    4.30 @@ -330,7 +330,7 @@
    4.31            Library.take (length newTs, reccomb_names)) ([], thy1)
    4.32        ||> Theory.checkpoint;
    4.33  
    4.34 -    val case_thms = map (map (fn t => SkipProof.prove_global thy2 [] [] t
    4.35 +    val case_thms = map (map (fn t => Skip_Proof.prove_global thy2 [] [] t
    4.36        (fn _ => EVERY [rewrite_goals_tac (case_defs @ map mk_meta_eq primrec_thms), rtac refl 1])))
    4.37            (DatatypeProp.make_cases new_type_names descr sorts thy2)
    4.38    in
    4.39 @@ -364,8 +364,8 @@
    4.40          val tacf = K (EVERY [rtac exhaustion' 1, ALLGOALS (asm_simp_tac
    4.41            (HOL_ss addsimps (dist_rewrites' @ inject @ case_thms')))])
    4.42        in
    4.43 -        (SkipProof.prove_global thy [] [] t1 tacf,
    4.44 -         SkipProof.prove_global thy [] [] t2 tacf)
    4.45 +        (Skip_Proof.prove_global thy [] [] t1 tacf,
    4.46 +         Skip_Proof.prove_global thy [] [] t2 tacf)
    4.47        end;
    4.48  
    4.49      val split_thm_pairs = map prove_split_thms
    4.50 @@ -384,7 +384,7 @@
    4.51  fun prove_weak_case_congs new_type_names descr sorts thy =
    4.52    let
    4.53      fun prove_weak_case_cong t =
    4.54 -       SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    4.55 +       Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    4.56           (fn {prems, ...} => EVERY [rtac ((hd prems) RS arg_cong) 1])
    4.57  
    4.58      val weak_case_congs = map prove_weak_case_cong (DatatypeProp.make_weak_case_congs
    4.59 @@ -405,7 +405,7 @@
    4.60                hyp_subst_tac i, REPEAT (rtac exI i), rtac refl i]
    4.61            | tac i n = rtac disjI2 i THEN tac i (n - 1)
    4.62        in 
    4.63 -        SkipProof.prove_global thy [] [] t (fn _ =>
    4.64 +        Skip_Proof.prove_global thy [] [] t (fn _ =>
    4.65            EVERY [rtac allI 1,
    4.66             exh_tac (K exhaustion) 1,
    4.67             ALLGOALS (fn i => tac i (i-1))])
    4.68 @@ -427,7 +427,7 @@
    4.69          val [v] = Term.add_vars (concl_of nchotomy') [];
    4.70          val nchotomy'' = cterm_instantiate [(cert (Var v), cert Ma)] nchotomy'
    4.71        in
    4.72 -        SkipProof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    4.73 +        Skip_Proof.prove_global thy [] (Logic.strip_imp_prems t) (Logic.strip_imp_concl t)
    4.74            (fn {prems, ...} => 
    4.75              let val simplify = asm_simp_tac (HOL_ss addsimps (prems @ case_rewrites))
    4.76              in EVERY [simp_tac (HOL_ss addsimps [hd prems]) 1,
     5.1 --- a/src/HOL/Tools/Datatype/datatype_codegen.ML	Sat Oct 17 16:40:41 2009 +0200
     5.2 +++ b/src/HOL/Tools/Datatype/datatype_codegen.ML	Sat Oct 17 16:58:03 2009 +0200
     5.3 @@ -384,7 +384,7 @@
     5.4      val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
     5.5      val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss addsimps 
     5.6        (map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
     5.7 -    fun prove prop = SkipProof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
     5.8 +    fun prove prop = Skip_Proof.prove_global thy [] [] prop (K (ALLGOALS (simp_tac simpset)))
     5.9        |> Simpdata.mk_eq;
    5.10    in map (rpair true o prove) (triv_injects @ injects @ distincts) @ [(prove refl, false)] end;
    5.11  
     6.1 --- a/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sat Oct 17 16:40:41 2009 +0200
     6.2 +++ b/src/HOL/Tools/Datatype/datatype_rep_proofs.ML	Sat Oct 17 16:58:03 2009 +0200
     6.3 @@ -344,7 +344,7 @@
     6.4          (* prove characteristic equations *)
     6.5  
     6.6          val rewrites = def_thms @ (map mk_meta_eq rec_rewrites);
     6.7 -        val char_thms' = map (fn eqn => SkipProof.prove_global thy' [] [] eqn
     6.8 +        val char_thms' = map (fn eqn => Skip_Proof.prove_global thy' [] [] eqn
     6.9            (fn _ => EVERY [rewrite_goals_tac rewrites, rtac refl 1])) eqns;
    6.10  
    6.11        in (thy', char_thms' @ char_thms) end;
    6.12 @@ -366,7 +366,7 @@
    6.13              val Ts = map (TFree o rpair HOLogic.typeS)
    6.14                (Name.variant_list used (replicate i "'t"));
    6.15              val f = Free ("f", Ts ---> U)
    6.16 -          in SkipProof.prove_global thy [] [] (Logic.mk_implies
    6.17 +          in Skip_Proof.prove_global thy [] [] (Logic.mk_implies
    6.18              (HOLogic.mk_Trueprop (HOLogic.list_all
    6.19                 (map (pair "x") Ts, S $ app_bnds f i)),
    6.20               HOLogic.mk_Trueprop (HOLogic.mk_eq (list_abs (map (pair "x") Ts,
    6.21 @@ -403,7 +403,7 @@
    6.22          val inj_thms' = map snd newT_iso_inj_thms @
    6.23            map (fn r => r RS @{thm injD}) inj_thms;
    6.24  
    6.25 -        val inj_thm = SkipProof.prove_global thy5 [] []
    6.26 +        val inj_thm = Skip_Proof.prove_global thy5 [] []
    6.27            (HOLogic.mk_Trueprop (mk_conj ind_concl1)) (fn _ => EVERY
    6.28              [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    6.29               REPEAT (EVERY
    6.30 @@ -429,7 +429,7 @@
    6.31                               (split_conj_thm inj_thm);
    6.32  
    6.33          val elem_thm = 
    6.34 -            SkipProof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    6.35 +            Skip_Proof.prove_global thy5 [] [] (HOLogic.mk_Trueprop (mk_conj ind_concl2))
    6.36                (fn _ =>
    6.37                 EVERY [(indtac induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    6.38                  rewrite_goals_tac rewrites,
    6.39 @@ -466,7 +466,7 @@
    6.40  
    6.41      val iso_thms = if length descr = 1 then [] else
    6.42        Library.drop (length newTs, split_conj_thm
    6.43 -        (SkipProof.prove_global thy5 [] [] iso_t (fn _ => EVERY
    6.44 +        (Skip_Proof.prove_global thy5 [] [] iso_t (fn _ => EVERY
    6.45             [(indtac rep_induct [] THEN_ALL_NEW ObjectLogic.atomize_prems_tac) 1,
    6.46              REPEAT (rtac TrueI 1),
    6.47              rewrite_goals_tac (mk_meta_eq choice_eq ::
    6.48 @@ -496,7 +496,7 @@
    6.49        let
    6.50          val inj_thms = map fst newT_iso_inj_thms;
    6.51          val rewrites = @{thm o_def} :: constr_defs @ (map (mk_meta_eq o #2) newT_iso_axms)
    6.52 -      in SkipProof.prove_global thy5 [] [] eqn (fn _ => EVERY
    6.53 +      in Skip_Proof.prove_global thy5 [] [] eqn (fn _ => EVERY
    6.54          [resolve_tac inj_thms 1,
    6.55           rewrite_goals_tac rewrites,
    6.56           rtac refl 3,
    6.57 @@ -520,7 +520,7 @@
    6.58          fun prove [] = []
    6.59            | prove (t :: ts) =
    6.60                let
    6.61 -                val dist_thm = SkipProof.prove_global thy5 [] [] t (fn _ =>
    6.62 +                val dist_thm = Skip_Proof.prove_global thy5 [] [] t (fn _ =>
    6.63                    EVERY [simp_tac (HOL_ss addsimps dist_rewrites') 1])
    6.64                in dist_thm :: Drule.standard (dist_thm RS not_sym) :: prove ts end;
    6.65        in prove ts end;
    6.66 @@ -535,7 +535,7 @@
    6.67          (iso_inj_thms @
    6.68            [In0_inject, In1_inject, Leaf_inject, Inl_inject, Inr_inject,
    6.69             Lim_inject, Suml_inject, Sumr_inject]))
    6.70 -      in SkipProof.prove_global thy5 [] [] t (fn _ => EVERY
    6.71 +      in Skip_Proof.prove_global thy5 [] [] t (fn _ => EVERY
    6.72          [rtac iffI 1,
    6.73           REPEAT (etac conjE 2), hyp_subst_tac 2, rtac refl 2,
    6.74           dresolve_tac rep_congs 1, dtac box_equals 1,
    6.75 @@ -585,7 +585,7 @@
    6.76  
    6.77      val cert = cterm_of thy6;
    6.78  
    6.79 -    val indrule_lemma = SkipProof.prove_global thy6 [] []
    6.80 +    val indrule_lemma = Skip_Proof.prove_global thy6 [] []
    6.81        (Logic.mk_implies
    6.82          (HOLogic.mk_Trueprop (mk_conj indrule_lemma_prems),
    6.83           HOLogic.mk_Trueprop (mk_conj indrule_lemma_concls))) (fn _ => EVERY
    6.84 @@ -600,7 +600,7 @@
    6.85      val indrule_lemma' = cterm_instantiate (map cert Ps ~~ map cert frees) indrule_lemma;
    6.86  
    6.87      val dt_induct_prop = DatatypeProp.make_ind descr sorts;
    6.88 -    val dt_induct = SkipProof.prove_global thy6 []
    6.89 +    val dt_induct = Skip_Proof.prove_global thy6 []
    6.90        (Logic.strip_imp_prems dt_induct_prop) (Logic.strip_imp_concl dt_induct_prop)
    6.91        (fn {prems, ...} => EVERY
    6.92          [rtac indrule_lemma' 1,
     7.1 --- a/src/HOL/Tools/Function/size.ML	Sat Oct 17 16:40:41 2009 +0200
     7.2 +++ b/src/HOL/Tools/Function/size.ML	Sat Oct 17 16:58:03 2009 +0200
     7.3 @@ -164,7 +164,7 @@
     7.4  
     7.5      fun prove_unfolded_size_eqs size_ofp fs =
     7.6        if null recTs2 then []
     7.7 -      else split_conj_thm (SkipProof.prove ctxt xs []
     7.8 +      else split_conj_thm (Skip_Proof.prove ctxt xs []
     7.9          (HOLogic.mk_Trueprop (mk_conj (replicate l HOLogic.true_const @
    7.10             map (mk_unfolded_size_eq (AList.lookup op =
    7.11                 (new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
    7.12 @@ -198,7 +198,7 @@
    7.13  
    7.14      fun prove_size_eqs p size_fns size_ofp simpset =
    7.15        maps (fn (((_, (_, _, constrs)), size_const), T) =>
    7.16 -        map (fn constr => Drule.standard (SkipProof.prove ctxt [] []
    7.17 +        map (fn constr => Drule.standard (Skip_Proof.prove ctxt [] []
    7.18            (gen_mk_size_eq p (AList.lookup op = (new_type_names ~~ size_fns))
    7.19               size_ofp size_const T constr)
    7.20            (fn _ => simp_tac simpset 1))) constrs)
     8.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 17 16:40:41 2009 +0200
     8.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_data.ML	Sat Oct 17 16:58:03 2009 +0200
     8.3 @@ -108,7 +108,7 @@
     8.4        in ((Free (x, T), HOLogic.mk_ptuple paths T (map Free xTs)), nctxt') end
     8.5      val (rewr, _) = fold_map mk_tuple_rewrites frees nctxt 
     8.6      val t' = Pattern.rewrite_term thy rewr [] t
     8.7 -    val tac = setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy)
     8.8 +    val tac = Skip_Proof.cheat_tac thy
     8.9      val th'' = Goal.prove ctxt (Term.add_free_names t' []) [] t' (fn {...} => tac)
    8.10      val th''' = LocalDefs.unfold ctxt [@{thm split_conv}] th''
    8.11    in
    8.12 @@ -117,7 +117,7 @@
    8.13  
    8.14  fun normalize_equation thy th =
    8.15    mk_meta_equation th
    8.16 -	|> Pred_Compile_Set.unfold_set_notation
    8.17 +  |> Pred_Compile_Set.unfold_set_notation
    8.18    |> full_fun_cong_expand
    8.19    |> split_all_pairs thy
    8.20    |> tap check_equation_format
     9.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Sat Oct 17 16:40:41 2009 +0200
     9.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML	Sat Oct 17 16:58:03 2009 +0200
     9.3 @@ -56,7 +56,7 @@
     9.4      val ((_, intros), ctxt') = Variable.import true intros ctxt
     9.5      val (intros', (local_defs, thy')) = (fold_map o fold_map_atoms)
     9.6        (flatten constname) (map prop_of intros) ([], thy)
     9.7 -    val tac = fn _ => setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy')
     9.8 +    val tac = fn _ => Skip_Proof.cheat_tac thy'
     9.9      val intros'' = map (fn t => Goal.prove ctxt' [] [] t tac) intros'
    9.10        |> Variable.export ctxt' ctxt
    9.11    in
    10.1 --- a/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 17 16:40:41 2009 +0200
    10.2 +++ b/src/HOL/Tools/Predicate_Compile/pred_compile_quickcheck.ML	Sat Oct 17 16:58:03 2009 +0200
    10.3 @@ -58,7 +58,7 @@
    10.4      val t = Logic.list_implies
    10.5        (map HOLogic.mk_Trueprop (prems @ [HOLogic.mk_not concl]),
    10.6         HOLogic.mk_Trueprop (list_comb (Const (full_constname, constT), map Free vs')))
    10.7 -    val tac = fn _ => setmp_CRITICAL quick_and_dirty true (SkipProof.cheat_tac thy')
    10.8 +    val tac = fn _ => Skip_Proof.cheat_tac thy'
    10.9      val intro = Goal.prove (ProofContext.init thy') (map fst vs') [] t tac
   10.10      val _ = tracing (Display.string_of_thm ctxt' intro)
   10.11      val thy'' = thy'
    11.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 17 16:40:41 2009 +0200
    11.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sat Oct 17 16:58:03 2009 +0200
    11.3 @@ -661,7 +661,7 @@
    11.4      val _ = tracing (commas (map (Display.string_of_thm_global thy) pre_intros))
    11.5      val nparams = guess_nparams T
    11.6      val pre_elim = 
    11.7 -      (Drule.standard o (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)))
    11.8 +      (Drule.standard o Skip_Proof.make_thm thy)
    11.9        (mk_casesrule (ProofContext.init thy) nparams pre_intros)
   11.10    in register_predicate (pre_intros, pre_elim, nparams) thy end
   11.11  
   11.12 @@ -2082,7 +2082,7 @@
   11.13          THEN print_tac "proved one direction"
   11.14          THEN prove_other_direction thy modes pred mode moded_clauses
   11.15          THEN print_tac "proved other direction")
   11.16 -      else (fn _ => setmp_CRITICAL quick_and_dirty true SkipProof.cheat_tac thy))
   11.17 +      else fn _ => Skip_Proof.cheat_tac thy)
   11.18    end;
   11.19  
   11.20  (* composition of mode inference, definition, compilation and proof *)
   11.21 @@ -2110,8 +2110,7 @@
   11.22      (join_preds_modes moded_clauses compiled_terms)
   11.23  
   11.24  fun prove_by_skip thy _ _ _ _ compiled_terms =
   11.25 -  map_preds_modes (fn pred => fn mode => fn t =>
   11.26 -      Drule.standard (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy) t))
   11.27 +  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
   11.28      compiled_terms
   11.29      
   11.30  fun prepare_intrs thy prednames =
    12.1 --- a/src/HOL/Tools/inductive.ML	Sat Oct 17 16:40:41 2009 +0200
    12.2 +++ b/src/HOL/Tools/inductive.ML	Sat Oct 17 16:58:03 2009 +0200
    12.3 @@ -321,7 +321,7 @@
    12.4  fun prove_mono quiet_mode skip_mono fork_mono predT fp_fun monos ctxt =
    12.5   (message (quiet_mode orelse skip_mono andalso !quick_and_dirty orelse fork_mono)
    12.6      "  Proving monotonicity ...";
    12.7 -  (if skip_mono then SkipProof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
    12.8 +  (if skip_mono then Skip_Proof.prove else if fork_mono then Goal.prove_future else Goal.prove) ctxt
    12.9      [] []
   12.10      (HOLogic.mk_Trueprop
   12.11        (Const (@{const_name Orderings.mono}, (predT --> predT) --> HOLogic.boolT) $ fp_fun))
   12.12 @@ -350,7 +350,7 @@
   12.13      val rules = [refl, TrueI, notFalseI, exI, conjI];
   12.14  
   12.15      val intrs = map_index (fn (i, intr) => rulify
   12.16 -      (SkipProof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY
   12.17 +      (Skip_Proof.prove ctxt (map (fst o dest_Free) params) [] intr (fn _ => EVERY
   12.18         [rewrite_goals_tac rec_preds_defs,
   12.19          rtac (unfold RS iffD2) 1,
   12.20          EVERY1 (select_disj (length intr_ts) (i + 1)),
   12.21 @@ -395,7 +395,7 @@
   12.22          val prems = HOLogic.mk_Trueprop (list_comb (c, params @ frees)) ::
   12.23             map mk_elim_prem (map #1 c_intrs)
   12.24        in
   12.25 -        (SkipProof.prove ctxt'' [] prems P
   12.26 +        (Skip_Proof.prove ctxt'' [] prems P
   12.27            (fn {prems, ...} => EVERY
   12.28              [cut_facts_tac [hd prems] 1,
   12.29               rewrite_goals_tac rec_preds_defs,
   12.30 @@ -558,7 +558,7 @@
   12.31  
   12.32      val raw_fp_induct = (mono RS (fp_def RS @{thm def_lfp_induct}));
   12.33  
   12.34 -    val induct = SkipProof.prove ctxt'' [] ind_prems ind_concl
   12.35 +    val induct = Skip_Proof.prove ctxt'' [] ind_prems ind_concl
   12.36        (fn {prems, ...} => EVERY
   12.37          [rewrite_goals_tac [inductive_conj_def],
   12.38           DETERM (rtac raw_fp_induct 1),
   12.39 @@ -575,7 +575,7 @@
   12.40               (inductive_conj_def :: rec_preds_defs @ simp_thms'') prem,
   12.41             conjI, refl] 1)) prems)]);
   12.42  
   12.43 -    val lemma = SkipProof.prove ctxt'' [] []
   12.44 +    val lemma = Skip_Proof.prove ctxt'' [] []
   12.45        (Logic.mk_implies (ind_concl, mutual_ind_concl)) (fn _ => EVERY
   12.46          [rewrite_goals_tac rec_preds_defs,
   12.47           REPEAT (EVERY
    13.1 --- a/src/HOL/Tools/quickcheck_generators.ML	Sat Oct 17 16:40:41 2009 +0200
    13.2 +++ b/src/HOL/Tools/quickcheck_generators.ML	Sat Oct 17 16:58:03 2009 +0200
    13.3 @@ -149,7 +149,7 @@
    13.4      val tac = ALLGOALS (rtac rule)
    13.5        THEN ALLGOALS (simp_tac rew_ss)
    13.6        THEN (ALLGOALS (ProofContext.fact_tac (flat eqs2)))
    13.7 -    val simp = SkipProof.prove lthy' [v] [] eq (K tac);
    13.8 +    val simp = Skip_Proof.prove lthy' [v] [] eq (K tac);
    13.9    in (simp, lthy') end;
   13.10  
   13.11  end;
   13.12 @@ -185,7 +185,7 @@
   13.13                ALLGOALS (simp_tac (HOL_ss addsimps proj_simps))
   13.14                THEN ALLGOALS (EqSubst.eqsubst_tac ctxt [0] [aux_simp])
   13.15                THEN ALLGOALS (simp_tac (HOL_ss addsimps [fst_conv, snd_conv]));
   13.16 -          in (map (fn prop => SkipProof.prove lthy [v] [] prop tac) eqs, lthy) end;
   13.17 +          in (map (fn prop => Skip_Proof.prove lthy [v] [] prop tac) eqs, lthy) end;
   13.18        in
   13.19          lthy
   13.20          |> random_aux_primrec aux_eq'
   13.21 @@ -206,7 +206,7 @@
   13.22        let
   13.23          val ext_simps = map (fn thm => fun_cong OF [fun_cong OF [thm]]) proto_simps;
   13.24          val tac = ALLGOALS (ProofContext.fact_tac ext_simps);
   13.25 -      in (map (fn prop => SkipProof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
   13.26 +      in (map (fn prop => Skip_Proof.prove lthy vs [] prop (K tac)) eqs, lthy) end;
   13.27      val b = Binding.qualify true prfx (Binding.qualify true name (Binding.name "simps"));
   13.28    in
   13.29      lthy
    14.1 --- a/src/HOL/Tools/record.ML	Sat Oct 17 16:40:41 2009 +0200
    14.2 +++ b/src/HOL/Tools/record.ML	Sat Oct 17 16:58:03 2009 +0200
    14.3 @@ -1040,7 +1040,7 @@
    14.4    if ! record_quick_and_dirty_sensitive andalso ! quick_and_dirty then
    14.5      Goal.prove (ProofContext.init thy) [] []
    14.6        (Logic.list_implies (map Logic.varify asms, Logic.varify prop))
    14.7 -      (K (SkipProof.cheat_tac @{theory HOL}))
    14.8 +      (K (Skip_Proof.cheat_tac @{theory HOL}))
    14.9        (*Drule.standard can take quite a while for large records, thats why
   14.10          we varify the proposition manually here.*)
   14.11    else
    15.1 --- a/src/HOL/Tools/sat_funcs.ML	Sat Oct 17 16:40:41 2009 +0200
    15.2 +++ b/src/HOL/Tools/sat_funcs.ML	Sat Oct 17 16:58:03 2009 +0200
    15.3 @@ -337,7 +337,7 @@
    15.4  		val _ = if !trace_sat then
    15.5  				tracing "'quick_and_dirty' is set: proof reconstruction skipped, using oracle instead."
    15.6  			else ()
    15.7 -		val False_thm = SkipProof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
    15.8 +		val False_thm = Skip_Proof.make_thm @{theory} (HOLogic.Trueprop $ HOLogic.false_const)
    15.9  	in
   15.10  		(* 'fold Thm.weaken (rev sorted_clauses)' is linear, while 'fold    *)
   15.11  		(* Thm.weaken sorted_clauses' would be quadratic, since we sorted   *)
    16.1 --- a/src/HOL/Tools/typedef.ML	Sat Oct 17 16:40:41 2009 +0200
    16.2 +++ b/src/HOL/Tools/typedef.ML	Sat Oct 17 16:58:03 2009 +0200
    16.3 @@ -199,8 +199,7 @@
    16.4  
    16.5      (*test theory errors now!*)
    16.6      val test_thy = Theory.copy thy;
    16.7 -    val _ = test_thy
    16.8 -      |> typedef_result (setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm test_thy) goal);
    16.9 +    val _ = typedef_result (Skip_Proof.make_thm test_thy goal) test_thy;
   16.10  
   16.11    in (set, goal, goal_pat, typedef_result) end
   16.12    handle ERROR msg =>
    17.1 --- a/src/HOL/ex/predicate_compile.ML	Sat Oct 17 16:40:41 2009 +0200
    17.2 +++ b/src/HOL/ex/predicate_compile.ML	Sat Oct 17 16:58:03 2009 +0200
    17.3 @@ -114,10 +114,10 @@
    17.4  val do_proofs = Unsynchronized.ref true;
    17.5  
    17.6  fun mycheat_tac thy i st =
    17.7 -  (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) i) st
    17.8 +  (Tactic.rtac (Skip_Proof.make_thm thy (Var (("A", 0), propT))) i) st
    17.9  
   17.10  fun remove_last_goal thy st =
   17.11 -  (Tactic.rtac (SkipProof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
   17.12 +  (Tactic.rtac (Skip_Proof.make_thm thy (Var (("A", 0), propT))) (nprems_of st)) st
   17.13  
   17.14  (* reference to preprocessing of InductiveSet package *)
   17.15  
   17.16 @@ -1866,7 +1866,7 @@
   17.17      (join_preds_modes moded_clauses compiled_terms)
   17.18  
   17.19  fun prove_by_skip thy _ _ _ _ compiled_terms =
   17.20 -  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (SkipProof.make_thm thy t))
   17.21 +  map_preds_modes (fn pred => fn mode => fn t => Drule.standard (Skip_Proof.make_thm thy t))
   17.22      compiled_terms
   17.23      
   17.24  fun prepare_intrs thy prednames =
    18.1 --- a/src/Pure/Isar/class.ML	Sat Oct 17 16:40:41 2009 +0200
    18.2 +++ b/src/Pure/Isar/class.ML	Sat Oct 17 16:58:03 2009 +0200
    18.3 @@ -76,7 +76,7 @@
    18.4          val ((_, [thm']), _) = Variable.import true [thm] empty_ctxt;
    18.5          val thm'' = Morphism.thm (const_morph $> eq_morph) thm';
    18.6          val tac = ALLGOALS (ProofContext.fact_tac [thm'']);
    18.7 -      in SkipProof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    18.8 +      in Skip_Proof.prove_global thy [] [] (Thm.prop_of thm'') (K tac) end;
    18.9      val assm_intro = Option.map prove_assm_intro
   18.10        (fst (Locale.intros_of thy class));
   18.11  
   18.12 @@ -93,7 +93,7 @@
   18.13        (Tactic.match_tac (axclass_intro :: sup_of_classes
   18.14           @ loc_axiom_intros @ base_sort_trivs)
   18.15             ORELSE' Tactic.assume_tac));
   18.16 -    val of_class = SkipProof.prove_global thy [] [] of_class_prop (K tac);
   18.17 +    val of_class = Skip_Proof.prove_global thy [] [] of_class_prop (K tac);
   18.18  
   18.19    in (base_morph, eq_morph, export_morph, axiom, assm_intro, of_class) end;
   18.20  
    19.1 --- a/src/Pure/Isar/class_target.ML	Sat Oct 17 16:40:41 2009 +0200
    19.2 +++ b/src/Pure/Isar/class_target.ML	Sat Oct 17 16:58:03 2009 +0200
    19.3 @@ -239,7 +239,7 @@
    19.4        [Option.map (Drule.standard' o Element.conclude_witness) some_wit,
    19.5          (fst o rules thy) sub];
    19.6      val tac = EVERY (map (TRYALL o Tactic.rtac) intros);
    19.7 -    val classrel = SkipProof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
    19.8 +    val classrel = Skip_Proof.prove_global thy [] [] (Logic.mk_classrel (sub, sup))
    19.9        (K tac);
   19.10      val diff_sort = Sign.complete_sort thy [sup]
   19.11        |> subtract (op =) (Sign.complete_sort thy [sub])
    20.1 --- a/src/Pure/Isar/skip_proof.ML	Sat Oct 17 16:40:41 2009 +0200
    20.2 +++ b/src/Pure/Isar/skip_proof.ML	Sat Oct 17 16:58:03 2009 +0200
    20.3 @@ -1,7 +1,8 @@
    20.4  (*  Title:      Pure/Isar/skip_proof.ML
    20.5      Author:     Markus Wenzel, TU Muenchen
    20.6  
    20.7 -Skipping proofs -- quick_and_dirty mode.
    20.8 +Skipping proofs -- via oracle (in quick and dirty mode) or by forking
    20.9 +(parallel mode).
   20.10  *)
   20.11  
   20.12  signature SKIP_PROOF =
   20.13 @@ -14,15 +15,13 @@
   20.14      ({prems: thm list, context: Proof.context} -> tactic) -> thm
   20.15  end;
   20.16  
   20.17 -structure SkipProof: SKIP_PROOF =
   20.18 +structure Skip_Proof: SKIP_PROOF =
   20.19  struct
   20.20  
   20.21  (* oracle setup *)
   20.22  
   20.23  val (_, skip_proof) = Context.>>> (Context.map_theory_result
   20.24 -  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) =>
   20.25 -    if ! quick_and_dirty then Thm.cterm_of thy prop
   20.26 -    else error "Proof may be skipped in quick_and_dirty mode only!")));
   20.27 +  (Thm.add_oracle (Binding.name "skip_proof", fn (thy, prop) => Thm.cterm_of thy prop)));
   20.28  
   20.29  
   20.30  (* basic cheating *)
   20.31 @@ -36,7 +35,7 @@
   20.32    (if Goal.future_enabled () then Goal.prove_future else Goal.prove) ctxt xs asms prop
   20.33      (fn args => fn st =>
   20.34        if ! quick_and_dirty
   20.35 -      then setmp_CRITICAL quick_and_dirty true (cheat_tac (ProofContext.theory_of ctxt)) st
   20.36 +      then cheat_tac (ProofContext.theory_of ctxt) st
   20.37        else tac args st);
   20.38  
   20.39  fun prove_global thy xs asms prop tac =
    21.1 --- a/src/Pure/codegen.ML	Sat Oct 17 16:40:41 2009 +0200
    21.2 +++ b/src/Pure/codegen.ML	Sat Oct 17 16:58:03 2009 +0200
    21.3 @@ -280,8 +280,7 @@
    21.4    let
    21.5      val x = Free (Name.variant (OldTerm.add_term_names (t, [])) "x", fastype_of t);
    21.6      (* fake definition *)
    21.7 -    val eq = setmp_CRITICAL quick_and_dirty true (SkipProof.make_thm thy)
    21.8 -      (Logic.mk_equals (x, t));
    21.9 +    val eq = Skip_Proof.make_thm thy (Logic.mk_equals (x, t));
   21.10      fun err () = error "preprocess_term: bad preprocessor"
   21.11    in case map prop_of (preprocess thy [eq]) of
   21.12        [Const ("==", _) $ x' $ t'] => if x = x' then t' else err ()