clarified name of Type.unified, to emphasize its connection to the "unify" family;
tuned low-level operation;

--- a/src/Pure/envir.ML	Sat Nov 08 16:55:41 2014 +0100
+++ b/src/Pure/envir.ML	Sat Nov 08 17:39:01 2014 +0100
@@ -124,7 +124,7 @@
   and use = instead of eq_type.*)
 fun lookup1 tenv = lookup_check (op =) tenv;
 
-fun lookup (Envir {tenv, tyenv, ...}) = lookup_check (Type.eq_type tyenv) tenv;
+fun lookup (Envir {tenv, tyenv, ...}) = lookup_check (Type.unified tyenv) tenv;
 
 fun update ((xi, T), t) (Envir {maxidx, tenv, tyenv}) =
   Envir {maxidx = maxidx, tenv = Vartab.update_new (xi, (T, t)) tenv, tyenv = tyenv};

--- a/src/Pure/type.ML	Sat Nov 08 16:55:41 2014 +0100
+++ b/src/Pure/type.ML	Sat Nov 08 17:39:01 2014 +0100
@@ -87,7 +87,7 @@
   val raw_unifys: typ list * typ list -> tyenv -> tyenv
   val could_unify: typ * typ -> bool
   val could_unifys: typ list * typ list -> bool
-  val eq_type: tyenv -> typ * typ -> bool
+  val unified: tyenv -> typ * typ -> bool
 
   (*extend and merge type signatures*)
   val add_class: Context.generic -> binding * class list -> tsig -> tsig
@@ -587,16 +587,17 @@
   | could_unifys ([], []) = true
   | could_unifys _ = false;
 
-
 (*equality with respect to a type environment*)
-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 (equal_type tye) (Ts, Ts')
-   | (U, U') => U = U');
-
-fun eq_type tye =
-  if Vartab.is_empty tye then op = else equal_type tye;
+fun unified tye =
+  let
+    fun unif (T, T') =
+      (case (devar tye T, devar tye T') of
+         (Type (s, Ts), Type (s', Ts')) => s = s' andalso unifs (Ts, Ts')
+       | (U, U') => U = U')
+    and unifs ([], []) = true
+      | unifs (T :: Ts, T' :: Ts') = unif (T', T') andalso unifs (Ts, Ts')
+      | unifs _ = false;
+  in if Vartab.is_empty tye then op = else unif end;