# HG changeset patch
# User wenzelm
# Date 1247859179 -7200
# Node ID 49d7d0bb90c60130f082eb5bcac2b94eaff5caa8
# Parent  94b4a921c88dd25d3e841465ccbbb6bf014de594
eq_type: special case for empty environment;

diff -r 94b4a921c88d -r 49d7d0bb90c6 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 **)