marked some CRITICAL sections;

--- a/src/Pure/General/source.ML	Mon Jul 23 16:45:00 2007 +0200
+++ b/src/Pure/General/source.ML	Mon Jul 23 16:45:01 2007 +0200
@@ -114,24 +114,26 @@
 
 (* stream source *)
 
-fun slurp_input instream =
+fun slurp_input instream = CRITICAL (fn () =>
   let
     fun slurp () =
       (case TextIO.canInput (instream, 1) handle IO.Io _ => NONE of
         NONE => []
       | SOME 0 => []
       | SOME _ => TextIO.input instream :: slurp ());
-  in maps explode (slurp ()) end;
+  in maps explode (slurp ()) end);
 
 fun drain_stream instream outstream prompt () =
   let val input = slurp_input instream in
     if exists (fn c => c = "\n") input then (input, ())
     else
-      (TextIO.output (outstream, Output.output prompt);
-        TextIO.flushOut outstream;
-        (case TextIO.inputLine instream of
+      (case
+        CRITICAL (fn () =>
+          (TextIO.output (outstream, Output.output prompt);
+            TextIO.flushOut outstream;
+            TextIO.inputLine instream)) of
           SOME line => (input @ explode line, ())
-        | NONE => (input, ())))
+        | NONE => (input, ()))
   end;
 
 fun of_stream instream outstream =

--- a/src/Pure/pure_thy.ML	Mon Jul 23 16:45:00 2007 +0200
+++ b/src/Pure/pure_thy.ML	Mon Jul 23 16:45:01 2007 +0200
@@ -304,11 +304,11 @@
 
 (* hiding -- affects current theory node only *)
 
-fun hide_thms fully names thy =
+fun hide_thms fully names thy = CRITICAL (fn () =>
   let
     val r as ref {theorems = (space, thms), index} = get_theorems_ref thy;
     val space' = fold (NameSpace.hide fully) names space;
-  in r := {theorems = (space', thms), index = index}; thy end;
+  in r := {theorems = (space', thms), index = index}; thy end);
 
 
 (* fact specifications *)
@@ -343,7 +343,7 @@
 fun warn_same name = warning ("Theorem database already contains a copy of " ^ quote name);
 
 fun enter_thms _ _ app_att ("", thms) thy = app_att (thy, thms) |> swap
-  | enter_thms pre_name post_name app_att (bname, thms) thy =
+  | enter_thms pre_name post_name app_att (bname, thms) thy = CRITICAL (fn () =>
       let
         val name = Sign.full_name thy bname;
         val (thy', thms') = apsnd (post_name name) (app_att (thy, pre_name name thms));
@@ -359,7 +359,7 @@
             else warn_overwrite name);
         r := {theorems = (space', theorems'), index = index'};
         (thms', thy')
-      end;
+      end);
 
 
 (* add_thms(s) *)