Removed some polymorphic equality tests
authorpaulson
Fri Mar 07 10:26:02 1997 +0100 (1997-03-07)
changeset 2753bcde71e5f371
parent 2752 74a9aead96c8
child 2754 59bd96046ad6
Removed some polymorphic equality tests
src/Pure/type.ML
src/Pure/unify.ML
     1.1 --- a/src/Pure/type.ML	Fri Mar 07 10:24:26 1997 +0100
     1.2 +++ b/src/Pure/type.ML	Fri Mar 07 10:26:02 1997 +0100
     1.3 @@ -816,7 +816,7 @@
     1.4  fun occ v tye =
     1.5    let fun occ(Type(_, Ts)) = exists occ Ts
     1.6          | occ(TFree _) = false
     1.7 -        | occ(TVar(w, _)) = v=w orelse
     1.8 +        | occ(TVar(w, _)) = eq_ix(v,w) orelse
     1.9                             (case assoc(tye, w) of
    1.10                                None   => false
    1.11                              | Some U => occ U);
    1.12 @@ -834,7 +834,7 @@
    1.13  
    1.14  fun add_to_tye(p,[]) = [p]
    1.15    | add_to_tye(vT as (v,T),(xU as (x,TVar(w,S)))::ps) =
    1.16 -      (if v=w then (x,T) else xU) :: (add_to_tye(vT,ps))
    1.17 +      (if eq_ix(v,w) then (x,T) else xU) :: (add_to_tye(vT,ps))
    1.18    | add_to_tye(v,x::xs) = x::(add_to_tye(v,xs));
    1.19  
    1.20  (* 'dom' returns for a type constructor t the list of those domains
    1.21 @@ -875,7 +875,7 @@
    1.22    let fun unif ((T, U), tye) =
    1.23          case (devar(T, tye), devar(U, tye)) of
    1.24            (T as TVar(v, S1), U as TVar(w, S2)) =>
    1.25 -             if v=w then tye else
    1.26 +             if eq_ix(v,w) then tye else
    1.27               if sortorder subclass (S1, S2) then add_to_tye((w, T),tye) else
    1.28               if sortorder subclass (S2, S1) then add_to_tye((v, U),tye)
    1.29               else let val nu = gen_tyvar (union_sort subclass (S1, S2))
     2.1 --- a/src/Pure/unify.ML	Fri Mar 07 10:24:26 1997 +0100
     2.2 +++ b/src/Pure/unify.ML	Fri Mar 07 10:26:02 1997 +0100
     2.3 @@ -146,7 +146,7 @@
     2.4  	| occur (Free _)  = false
     2.5  	| occur (Var (w,_))  = 
     2.6  	    if mem_ix (w, !seen) then false
     2.7 -	    else if v=w then true
     2.8 +	    else if eq_ix(v,w) then true
     2.9  	      (*no need to lookup: v has no assignment*)
    2.10  	    else (seen := w:: !seen;  
    2.11  	          case  Envir.lookup(env,w)  of
    2.12 @@ -209,7 +209,7 @@
    2.13  	| occur (Free _)  = NoOcc
    2.14  	| occur (Var (w,_))  = 
    2.15  	    if mem_ix (w, !seen) then NoOcc
    2.16 -	    else if v=w then Rigid
    2.17 +	    else if eq_ix(v,w) then Rigid
    2.18  	    else (seen := w:: !seen;  
    2.19  	          case  Envir.lookup(env,w)  of
    2.20  		      None    => NoOcc
    2.21 @@ -218,7 +218,7 @@
    2.22  	| occur (t as f$_) =  (*switch to nonrigid search?*)
    2.23  	   (case head_of_in (env,f) of
    2.24  	      Var (w,_) => (*w is not assigned*)
    2.25 -		if v=w then Rigid  
    2.26 +		if eq_ix(v,w) then Rigid  
    2.27  		else  nonrigid t
    2.28  	    | Abs(_,_,body) => nonrigid t (*not in normal form*)
    2.29  	    | _ => occomb t)
    2.30 @@ -593,7 +593,7 @@
    2.31    let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
    2.32    in  case  (head_of t, head_of u) of
    2.33        (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
    2.34 -	if v=w then		(*...occur check would falsely return true!*)
    2.35 +	if eq_ix(v,w) then     (*...occur check would falsely return true!*)
    2.36  	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
    2.37  	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
    2.38  	else if xless(v,w) then (*prefer to update the LARGER variable*)