src/HOL/Tools/Predicate_Compile/pred_compile_pred.ML

     fun flat_intro intro (new_defs, thy) =
       let
         val constname = fst (dest_Const (fst (strip_comb
           (HOLogic.dest_Trueprop (Logic.strip_imp_concl (prop_of intro))))))
         val (intro_ts, (new_defs, thy)) = fold_map_atoms (process constname) (prop_of intro) (new_defs, thy)
-        val th = setmp quick_and_dirty true (SkipProof.make_thm thy) intro_ts
+        val th = Skip_Proof.make_thm thy intro_ts
       in
         (th, (new_defs, thy))
       end
     fun fold_map_spec f [] s = ([], s)
       | fold_map_spec f ((c, ths) :: specs) s =