# HG changeset patch
# User paulson
# Date 846858321 -3600
# Node ID ddb8499c772b2410938a83bd82d76e99dc81ecd6
# Parent  093bbe6d333bfef0012ad6e9469f9888f9eefe71
Replaced foldl nodup_TVars by nodup_TVars_list -- for a big speedup on Poly/ML

diff -r 093bbe6d333b -r ddb8499c772b src/Pure/sign.ML
--- a/src/Pure/sign.ML	Fri Nov 01 15:15:39 1996 +0100
+++ b/src/Pure/sign.ML	Fri Nov 01 15:25:21 1996 +0100
@@ -222,7 +222,7 @@
 
 (* check for duplicate TVars with distinct sorts *)
 fun nodup_TVars(tvars,T) = (case T of
-      Type(_,Ts) => foldl nodup_TVars (tvars,Ts)
+      Type(_,Ts) => nodup_TVars_list (tvars,Ts)
     | TFree _ => tvars
     | TVar(v as (a,S)) =>
         (case assoc_string_int(tvars,a) of
@@ -230,7 +230,11 @@
                        else raise_type
                             ("Type variable "^Syntax.string_of_vname a^
                              " has two distinct sorts") [TVar(a,S'),T] []
-         | None => v::tvars));
+         | None => v::tvars))
+and (*equivalent to foldl nodup_TVars_list, but 3X faster under Poly/ML*)
+    nodup_TVars_list (tvars,[]) = tvars
+  | nodup_TVars_list (tvars,T::Ts) = nodup_TVars_list(nodup_TVars(tvars,T), 
+						      Ts);
 
 (* check for duplicate Vars with distinct types *)
 fun nodup_Vars tm =