marked some CRITICAL sections;

--- a/src/HOL/ex/Random.thy	Sun Jul 29 14:29:58 2007 +0200
+++ b/src/HOL/ex/Random.thy	Sun Jul 29 14:29:59 2007 +0200
@@ -156,12 +156,12 @@
 local
   val seed_ref = ref (fromInt 1);
 in
-  fun seed () =
+  fun seed () = CRITICAL (fn () =>
     let
       val r = next (!seed_ref)
     in
       (seed_ref := r; r)
-    end;
+    end);
 end;
 
 fun value h s =

--- a/src/HOLCF/Tools/cont_proc.ML	Sun Jul 29 14:29:58 2007 +0200
+++ b/src/HOLCF/Tools/cont_proc.ML	Sun Jul 29 14:29:59 2007 +0200
@@ -101,17 +101,18 @@
 local
   val rules = [cont_K, cont_I, cont_R, cont_A, cont_L];
   
+  (* FIXME proper cache as theory data!? *)
   val prev_cont_thms : thm list ref = ref [];
 
-  fun old_cont_tac i thm =
+  fun old_cont_tac i thm = CRITICAL (fn () =>
     case !prev_cont_thms of
       [] => no_tac thm
-    | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
+    | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
 
-  fun new_cont_tac f' i thm =
+  fun new_cont_tac f' i thm = CRITICAL (fn () =>
     case all_cont_thms f' of
       [] => no_tac thm
-    | (c::cs) => (prev_cont_thms := cs; rtac c i thm);
+    | (c::cs) => (prev_cont_thms := cs; rtac c i thm));
 
   fun cont_tac_of_term (Const ("Cont.cont", _) $ f) =
     let