# HG changeset patch
# User wenzelm
# Date 1222536900 -7200
# Node ID 74c6d73a8b2e20b566a89b2a9f2959f1fe3b1d44
# Parent  70abca69247be3d7455b87fe25ff15b0774e8a01
setmp_noncritical;

diff -r 70abca69247b -r 74c6d73a8b2e 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",