--- 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"];