diff -r f59857e32972 -r c0f6a1887518 src/Pure/term.ML
--- a/src/Pure/term.ML	Fri Dec 22 10:38:27 1995 +0100
+++ b/src/Pure/term.ML	Fri Dec 22 10:48:59 1995 +0100
@@ -593,6 +593,79 @@
 
 fun rename_wrt_term t = rename_aTs (add_term_names(t,[]));
 
+
+
+(*** Compression of terms and types by sharing common subtrees.  Currently
+     naive but could be made to run faster.  Saves 50-75% on storage  
+     requirements.  As it is slow, should be called only for axioms, stored
+     theorems, etc. ***)
+
+(** Sharing of types **)
+
+(*Allow non-"fun" types??*)
+fun atomic_tag (Type (a,_)) = if a<>"fun" then a else raise Match
+  | atomic_tag (TFree (a,_)) = a
+  | atomic_tag (TVar ((a,_),_)) = a;
+
+fun type_tag (Type("fun",[S,T])) = atomic_tag S ^ type_tag T
+  | type_tag T = atomic_tag T;
+
+val memo_types = ref (Symtab.null : typ list Symtab.table);
+
+fun find_type (T, []: typ list) = None
+  | find_type (T, T'::Ts) =
+       if T=T' then Some T'
+       else find_type (T, Ts);
+
+fun compress_type T =
+  let val tag = type_tag T
+      val tylist = the (Symtab.lookup (!memo_types, tag))
+	           handle _ => []
+  in  
+      case find_type (T,tylist) of
+	Some T' => T'
+      | None => 
+	    let val T' =
+		case T of
+		    Type (a,Ts) => Type (a, map compress_type Ts)
+		  | _ => T
+	    in  memo_types := Symtab.update ((tag, T'::tylist), !memo_types);
+		T
+	    end
+  end
+  handle Match =>
+      let val Type (a,Ts) = T
+      in  Type (a, map compress_type Ts)  end;
+
+(** Sharing of atomic terms **)
+
+val memo_terms = ref (Symtab.null : term list Symtab.table);
+
+fun find_term (t, []: term list) = None
+  | find_term (t, t'::ts) =
+       if t=t' then Some t'
+       else find_term (t, ts);
+
+fun const_tag (Const (a,_)) = a
+  | const_tag (Free (a,_))  = a
+  | const_tag (Var ((a,i),_)) = a
+  | const_tag (t as Bound _)  = ".B.";
+
+fun share_term (t $ u) = share_term t $ share_term u
+  | share_term (Abs (a,T,u)) = Abs (a, T, share_term u)
+  | share_term t =
+      let val tag = const_tag t
+	  val ts = the (Symtab.lookup (!memo_terms, tag))
+	               handle _ => []
+      in 
+	  case find_term (t,ts) of
+	      Some t' => t'
+	    | None => (memo_terms := Symtab.update ((tag, t::ts), !memo_terms);
+		       t)
+      end;
+
+val compress_term = share_term o map_term_types compress_type;
+
 end;
 
 open Term;