diff -r 0cf2749e8ef7 -r 7ff939586e83 src/HOL/Import/HOL/ROOT.ML
--- a/src/HOL/Import/HOL/ROOT.ML	Wed Oct 08 18:09:36 2008 +0200
+++ b/src/HOL/Import/HOL/ROOT.ML	Wed Oct 08 19:20:29 2008 +0200
@@ -4,5 +4,5 @@
 *)
 
 use_thy "Primes";
-setmp quick_and_dirty true use_thy "HOL4Prob";
-setmp quick_and_dirty true use_thy "HOL4";
+setmp_noncritical quick_and_dirty true use_thy "HOL4Prob";
+setmp_noncritical quick_and_dirty true use_thy "HOL4";