setmp_noncritical;
authorwenzelm
Sat, 27 Sep 2008 19:35:00 +0200
changeset 28385 74c6d73a8b2e
parent 28384 70abca69247b
child 28386 f2f1dd50da5a
setmp_noncritical;
src/HOL/Induct/ROOT.ML
--- a/src/HOL/Induct/ROOT.ML	Sat Sep 27 18:18:08 2008 +0200
+++ b/src/HOL/Induct/ROOT.ML	Sat Sep 27 19:35:00 2008 +0200
@@ -1,7 +1,7 @@
 
 (* $Id$ *)
 
-setmp quick_and_dirty true
+setmp_noncritical quick_and_dirty true
   use_thy "Common_Patterns";
 
 use_thys ["Mutil", "QuoDataType", "QuoNestedDataType", "Term",