obsolete -- Poly/ML images are maximally shared already, home-grown compression wastes space and time;

--- a/src/Pure/compress.ML	Sat Apr 12 17:00:42 2008 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-(*  Title:      Pure/compress.ML
-    ID:         $Id$
-    Author:     Lawrence C Paulson and Makarius
-
-Compression of terms and types by sharing common subtrees.  Saves
-50-75% on storage requirements.  As it is a bit slow, it should be
-called only for axioms, stored theorems, etc.
-*)
-
-signature COMPRESS =
-sig
-  val typ: theory -> typ -> typ
-  val term: theory -> term -> term
-end;
-
-structure Compress: COMPRESS =
-struct
-
-
-(* theory data *)
-
-structure CompressData = TheoryDataFun
-(
-  type T = typ Typtab.table ref * term Termtab.table ref;
-  val empty : T = (ref Typtab.empty, ref Termtab.empty);
-  fun copy (ref typs, ref terms) : T = (ref typs, ref terms);
-  val extend = copy;
-  fun merge _ ((ref typs1, ref terms1), (ref typs2, ref terms2)) : T =
-   (ref (Typtab.merge (K true) (typs1, typs2)),
-    ref (Termtab.merge (K true) (terms1, terms2)));
-);
-
-val _ = Context.>> (Context.map_theory CompressData.init);
-
-
-(* compress types *)
-
-fun typ thy =
-  let
-    val typs = #1 (CompressData.get thy);
-    fun compress T =
-      (case Typtab.lookup (! typs) T of
-        SOME T' => T'
-      | NONE =>
-          let val T' = (case T of Type (a, Ts) => Type (a, map compress Ts) | _ => T)
-          in change typs (Typtab.update (T', T')); T' end);
-  in compress end;
-
-
-(* compress atomic terms *)
-
-fun term thy =
-  let
-    val terms = #2 (CompressData.get thy);
-    fun compress (t $ u) = compress t $ compress u
-      | compress (Abs (a, T, t)) = Abs (a, T, compress t)
-      | compress t =
-          (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;
-
-end;