src/Pure/term.ML
changeset 16599 34f99c3221bb
parent 16589 24c32abc8b84
child 16667 f56080acd176
     1.1 --- a/src/Pure/term.ML	Wed Jun 29 15:13:28 2005 +0200
     1.2 +++ b/src/Pure/term.ML	Wed Jun 29 15:13:29 2005 +0200
     1.3 @@ -403,10 +403,13 @@
     1.4    | head_of u = u;
     1.5  
     1.6  
     1.7 -(*Number of atoms and abstractions in a term*)
     1.8 -fun size_of_term (Abs (_,_,body)) = 1 + size_of_term body
     1.9 -  | size_of_term (f$t) = size_of_term f  +  size_of_term t
    1.10 -  | size_of_term _ = 1;
    1.11 +(*number of atoms and abstractions in a term*)
    1.12 +fun size_of_term tm =
    1.13 +  let
    1.14 +    fun add_size (t $ u) n = add_size t (add_size u n)
    1.15 +      | add_size (Abs (_ ,_, t)) n = add_size t (n + 1)
    1.16 +      | add_size _ n = n + 1;
    1.17 +  in add_size tm 0 end;
    1.18  
    1.19  fun map_type_tvar f (Type(a,Ts)) = Type(a, map (map_type_tvar f) Ts)
    1.20    | map_type_tvar f (T as TFree _) = T
    1.21 @@ -442,7 +445,9 @@
    1.22  fun indexname_ord ((x, i), (y, j)) =
    1.23    (case int_ord (i, j) of EQUAL => string_ord (x, y) | ord => ord);
    1.24  
    1.25 -val sort_ord = list_ord string_ord;
    1.26 +fun sort_ord SS =
    1.27 +  if pointer_eq SS then EQUAL
    1.28 +  else list_ord string_ord SS;
    1.29  
    1.30  
    1.31  (* typ_ord *)