non-critical (accidental concurrent access does not affect functional integrity);

--- a/src/Pure/compress.ML	Tue Dec 18 19:54:30 2007 +0100
+++ b/src/Pure/compress.ML	Tue Dec 18 19:54:31 2007 +0100
@@ -36,7 +36,7 @@
 
 (* compress types *)
 
-fun compress_typ thy =
+fun typ thy =
   let
     val typs = #1 (CompressData.get thy);
     fun compress T =
@@ -47,12 +47,10 @@
           in change typs (Typtab.update (T', T')); T' end);
   in compress end;
 
-fun typ ty = NAMED_CRITICAL "compress" (fn () => compress_typ ty);
-
 
 (* compress atomic terms *)
 
-fun compress_term thy =
+fun term thy =
   let
     val terms = #2 (CompressData.get thy);
     fun compress (t $ u) = compress t $ compress u
@@ -61,8 +59,6 @@
           (case Termtab.lookup (! terms) t of
             SOME t' => t'
           | NONE => (change terms (Termtab.update (t, t)); t));
-  in compress o map_types (compress_typ thy) end;
-
-fun term tm = NAMED_CRITICAL "compress" (fn () => compress_term tm);
+  in compress o map_types (typ thy) end;
 
 end;