src/Pure/type.ML

 
 (*Occurs check: type variable occurs in type?*)
 fun occ v tye =
   let fun occ(Type(_, Ts)) = exists occ Ts
         | occ(TFree _) = false
-        | occ(TVar(w, _)) = v=w orelse
+        | occ(TVar(w, _)) = eq_ix(v,w) orelse
                            (case assoc(tye, w) of
                               None   => false
                             | Some U => occ U);
   in occ end;
 

 (* use add_to_tye(t,tye) instead of t::tye
 to avoid chains of the form 'a |-> 'b |-> 'c ... *)
 
 fun add_to_tye(p,[]) = [p]
   | add_to_tye(vT as (v,T),(xU as (x,TVar(w,S)))::ps) =
-      (if v=w then (x,T) else xU) :: (add_to_tye(vT,ps))
+      (if eq_ix(v,w) then (x,T) else xU) :: (add_to_tye(vT,ps))
   | add_to_tye(v,x::xs) = x::(add_to_tye(v,xs));
 
 (* 'dom' returns for a type constructor t the list of those domains
    which deliver a given range class C *)
 

 (* Precondition: both types are well-formed w.r.t. type constructor arities *)
 fun unify1 (tsig as TySg{subclass, arities, ...}) =
   let fun unif ((T, U), tye) =
         case (devar(T, tye), devar(U, tye)) of
           (T as TVar(v, S1), U as TVar(w, S2)) =>
-             if v=w then tye else
+             if eq_ix(v,w) then tye else
              if sortorder subclass (S1, S2) then add_to_tye((w, T),tye) else
              if sortorder subclass (S2, S1) then add_to_tye((v, U),tye)
              else let val nu = gen_tyvar (union_sort subclass (S1, S2))
                   in add_to_tye((v, nu),add_to_tye((w, nu),tye)) end
         | (T as TVar(v, S), U) =>