src/Pure/type.ML

--- a/src/Pure/type.ML	Fri Jul 17 21:32:58 2009 +0200
+++ b/src/Pure/type.ML	Fri Jul 17 21:32:59 2009 +0200
@@ -494,12 +494,15 @@
 
 
 (*equality with respect to a type environment*)
-fun eq_type tye (T, T') =
+fun equal_type tye (T, T') =
   (case (devar tye T, devar tye T') of
      (Type (s, Ts), Type (s', Ts')) =>
-       s = s' andalso ListPair.all (eq_type tye) (Ts, Ts')
+       s = s' andalso ListPair.all (equal_type tye) (Ts, Ts')
    | (U, U') => U = U');
 
+fun eq_type tye =
+  if Vartab.is_empty tye then op = else equal_type tye;
+
 
 
 (** extend and merge type signatures **)