src/HOL/UNITY/ROOT.ML
changeset 28529 7ff939586e83
parent 24147 edc90be09ac1
child 28866 30cd9d89a0fb
--- 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"];