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 =>