--- a/src/Pure/compress.ML Mon Jul 23 14:06:11 2007 +0200
+++ b/src/Pure/compress.ML Mon Jul 23 14:06:12 2007 +0200
@@ -36,7 +36,7 @@
(* compress types *)
-fun typ thy =
+fun compress_typ thy =
let
val typs = #1 (CompressData.get thy);
fun compress T =
@@ -47,10 +47,12 @@
in change typs (Typtab.update (T', T')); T' end);
in compress end;
+fun typ ty = CRITICAL (fn () => compress_typ ty);
+
(* compress atomic terms *)
-fun term thy =
+fun compress_term thy =
let
val terms = #2 (CompressData.get thy);
fun compress (t $ u) = compress t $ compress u
@@ -59,6 +61,8 @@
(case Termtab.lookup (! terms) t of
SOME t' => t'
| NONE => (change terms (Termtab.update (t, t)); t));
- in compress o map_types (typ thy) end;
+ in compress o map_types (compress_typ thy) end;
+
+fun term tm = CRITICAL (fn () => compress_term tm);
end;