# HG changeset patch
# User paulson
# Date 820150565 -3600
# Node ID c60e9e1a1a23ac9cc9646b05a4718ef29ad6f4d2
# Parent  7b61bcfeaa950ece5ce81b2b3521ad275e06be31
Updated comments for compression functions

diff -r 7b61bcfeaa95 -r c60e9e1a1a23 src/Pure/term.ML
--- a/src/Pure/term.ML	Thu Dec 28 11:59:40 1995 +0100
+++ b/src/Pure/term.ML	Thu Dec 28 12:36:05 1995 +0100
@@ -595,14 +595,12 @@
 
 
 
-(*** 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. ***)
+(*** Compression of terms and types by sharing common subtrees.  
+     Saves 50-75% on storage requirements.  As it is fairly slow, 
+     it is 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;