# HG changeset patch
# User wenzelm
# Date 1185394852 -7200
# Node ID 72a9b436af5677e6644dbc0b75e11312d75773a6
# Parent  d7df8545f9f6d2672bb989cdea9b664fc6f466be
renamed CRITICAL' to NAMED_CRITICAL;

diff -r d7df8545f9f6 -r 72a9b436af56 src/Pure/ML-Systems/multithreading_dummy.ML
--- a/src/Pure/ML-Systems/multithreading_dummy.ML	Wed Jul 25 22:20:51 2007 +0200
+++ b/src/Pure/ML-Systems/multithreading_dummy.ML	Wed Jul 25 22:20:52 2007 +0200
@@ -19,7 +19,7 @@
   val available: bool
   val max_threads: int ref
   val self_critical: unit -> bool
-  val CRITICAL': string -> (unit -> 'a) -> 'a
+  val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
   val CRITICAL: (unit -> 'a) -> 'a
   val schedule: int -> ('a -> (Task.task * ('a -> 'a)) * 'a) -> 'a -> exn list
 end;
@@ -34,12 +34,12 @@
 val max_threads = ref 1;
 
 fun self_critical () = false;
-fun CRITICAL' _ e = e ();
+fun NAMED_CRITICAL _ e = e ();
 fun CRITICAL e = e ();
 
 fun schedule _ _ _ = raise Fail "Multithreading support unavailable";
 
 end;
 
-val CRITICAL' = Multithreading.CRITICAL';
+val NAMED_CRITICAL = Multithreading.NAMED_CRITICAL;
 val CRITICAL = Multithreading.CRITICAL;