# HG changeset patch
# User paulson
# Date 857726762 -3600
# Node ID bcde71e5f3714318323cbb768d954575cfa732cc
# Parent  74a9aead96c804303d907c32abe78b69c57f425e
Removed some polymorphic equality tests

diff -r 74a9aead96c8 -r bcde71e5f371 src/Pure/type.ML
--- a/src/Pure/type.ML	Fri Mar 07 10:24:26 1997 +0100
+++ b/src/Pure/type.ML	Fri Mar 07 10:26:02 1997 +0100
@@ -816,7 +816,7 @@
 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);
@@ -834,7 +834,7 @@
 
 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
@@ -875,7 +875,7 @@
   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))
diff -r 74a9aead96c8 -r bcde71e5f371 src/Pure/unify.ML
--- a/src/Pure/unify.ML	Fri Mar 07 10:24:26 1997 +0100
+++ b/src/Pure/unify.ML	Fri Mar 07 10:26:02 1997 +0100
@@ -146,7 +146,7 @@
 	| occur (Free _)  = false
 	| occur (Var (w,_))  = 
 	    if mem_ix (w, !seen) then false
-	    else if v=w then true
+	    else if eq_ix(v,w) then true
 	      (*no need to lookup: v has no assignment*)
 	    else (seen := w:: !seen;  
 	          case  Envir.lookup(env,w)  of
@@ -209,7 +209,7 @@
 	| occur (Free _)  = NoOcc
 	| occur (Var (w,_))  = 
 	    if mem_ix (w, !seen) then NoOcc
-	    else if v=w then Rigid
+	    else if eq_ix(v,w) then Rigid
 	    else (seen := w:: !seen;  
 	          case  Envir.lookup(env,w)  of
 		      None    => NoOcc
@@ -218,7 +218,7 @@
 	| occur (t as f$_) =  (*switch to nonrigid search?*)
 	   (case head_of_in (env,f) of
 	      Var (w,_) => (*w is not assigned*)
-		if v=w then Rigid  
+		if eq_ix(v,w) then Rigid  
 		else  nonrigid t
 	    | Abs(_,_,body) => nonrigid t (*not in normal form*)
 	    | _ => occomb t)
@@ -593,7 +593,7 @@
   let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
   in  case  (head_of t, head_of u) of
       (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
-	if v=w then		(*...occur check would falsely return true!*)
+	if eq_ix(v,w) then     (*...occur check would falsely return true!*)
 	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
 	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
 	else if xless(v,w) then (*prefer to update the LARGER variable*)