src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML

--- a/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 23:57:42 2009 +0200
+++ b/src/HOL/Tools/Predicate_Compile/pred_compile_aux.ML	Sat Oct 24 20:27:26 2009 +0200
@@ -121,7 +121,7 @@
 (* lifting term operations to theorems *)
 
 fun map_term thy f th =
-  setmp quick_and_dirty true (SkipProof.make_thm thy) (f (prop_of th))
+  Skip_Proof.make_thm thy (f (prop_of th))
 
 (*
 fun equals_conv lhs_cv rhs_cv ct =