src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML

     val (c, T) = dest_Const (fst (strip_intro_concl 0 (prop_of (hd pre_intros))))
     val _ = tracing ("Registering introduction rules of " ^ c)
     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
 
 fun set_generator_name pred mode name = 
   let

         THEN print_tac "after pred_iffI"
         THEN prove_one_direction thy clauses preds modes pred mode moded_clauses
         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 *)
 
 (** auxillary combinators for table of preds and modes **)

 fun prove thy clauses preds modes moded_clauses compiled_terms =
   map_preds_modes (prove_pred thy clauses preds modes)
     (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 =
   let
     val intrs = maps (intros_of thy) prednames