setmp_noncritical makes it work with future scheduler;
authorwenzelm
Wed, 08 Oct 2008 19:20:29 +0200
changeset 28529 7ff939586e83
parent 28528 0cf2749e8ef7
child 28530 843b35caa8c4
setmp_noncritical makes it work with future scheduler;
src/HOL/Import/HOL/ROOT.ML
src/HOL/UNITY/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";
--- 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"];