Replaced foldl nodup_TVars by nodup_TVars_list -- for a big speedup on Poly/ML
authorpaulson
Fri Nov 01 15:25:21 1996 +0100 (1996-11-01)
changeset 2144ddb8499c772b
parent 2143 093bbe6d333b
child 2145 5e8db0bc195e
Replaced foldl nodup_TVars by nodup_TVars_list -- for a big speedup on Poly/ML
src/Pure/sign.ML
     1.1 --- a/src/Pure/sign.ML	Fri Nov 01 15:15:39 1996 +0100
     1.2 +++ b/src/Pure/sign.ML	Fri Nov 01 15:25:21 1996 +0100
     1.3 @@ -222,7 +222,7 @@
     1.4  
     1.5  (* check for duplicate TVars with distinct sorts *)
     1.6  fun nodup_TVars(tvars,T) = (case T of
     1.7 -      Type(_,Ts) => foldl nodup_TVars (tvars,Ts)
     1.8 +      Type(_,Ts) => nodup_TVars_list (tvars,Ts)
     1.9      | TFree _ => tvars
    1.10      | TVar(v as (a,S)) =>
    1.11          (case assoc_string_int(tvars,a) of
    1.12 @@ -230,7 +230,11 @@
    1.13                         else raise_type
    1.14                              ("Type variable "^Syntax.string_of_vname a^
    1.15                               " has two distinct sorts") [TVar(a,S'),T] []
    1.16 -         | None => v::tvars));
    1.17 +         | None => v::tvars))
    1.18 +and (*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
    1.19 +    nodup_TVars_list (tvars,[]) = tvars
    1.20 +  | nodup_TVars_list (tvars,T::Ts) = nodup_TVars_list(nodup_TVars(tvars,T), 
    1.21 +						      Ts);
    1.22  
    1.23  (* check for duplicate Vars with distinct types *)
    1.24  fun nodup_Vars tm =