# HG changeset patch
# User wenzelm
# Date 1223486429 -7200
# Node ID 7ff939586e8398a3ec52ec20a9f428c7c4c31f01
# Parent  0cf2749e8ef730dbcebe424485424a4b8ff9a534
setmp_noncritical makes it work with future scheduler;

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";
diff -r 0cf2749e8ef7 -r 7ff939586e83 src/HOL/UNITY/ROOT.ML
--- a/src/HOL/UNITY/ROOT.ML	Wed Oct 08 18:09:36 2008 +0200
+++ b/src/HOL/UNITY/ROOT.ML	Wed Oct 08 19:20:29 2008 +0200
@@ -43,7 +43,7 @@
 
 (*Allocator example*)
 (* FIXME some parts no longer work -- had been commented out for a long time *)
-setmp quick_and_dirty true
+setmp_noncritical quick_and_dirty true
   use_thy "Comp/Alloc";
 
 use_thys ["Comp/AllocImpl", "Comp/Client"];