Updated comments for compression functions
authorpaulson
Thu Dec 28 12:36:05 1995 +0100 (1995-12-28)
changeset 1426c60e9e1a1a23
parent 1425 7b61bcfeaa95
child 1427 ecd90b82ab8e
Updated comments for compression functions
src/Pure/term.ML
     1.1 --- a/src/Pure/term.ML	Thu Dec 28 11:59:40 1995 +0100
     1.2 +++ b/src/Pure/term.ML	Thu Dec 28 12:36:05 1995 +0100
     1.3 @@ -595,14 +595,12 @@
     1.4  
     1.5  
     1.6  
     1.7 -(*** Compression of terms and types by sharing common subtrees.  Currently
     1.8 -     naive but could be made to run faster.  Saves 50-75% on storage  
     1.9 -     requirements.  As it is slow, should be called only for axioms, stored
    1.10 -     theorems, etc. ***)
    1.11 +(*** Compression of terms and types by sharing common subtrees.  
    1.12 +     Saves 50-75% on storage requirements.  As it is fairly slow, 
    1.13 +     it is called only for axioms, stored theorems, etc. ***)
    1.14  
    1.15  (** Sharing of types **)
    1.16  
    1.17 -(*Allow non-"fun" types??*)
    1.18  fun atomic_tag (Type (a,_)) = if a<>"fun" then a else raise Match
    1.19    | atomic_tag (TFree (a,_)) = a
    1.20    | atomic_tag (TVar ((a,_),_)) = a;