src/Pure/unify.ML
changeset 2753 bcde71e5f371
parent 2193 b7e59795c75b
child 3991 4cb2f2422695
     1.1 --- a/src/Pure/unify.ML	Fri Mar 07 10:24:26 1997 +0100
     1.2 +++ b/src/Pure/unify.ML	Fri Mar 07 10:26:02 1997 +0100
     1.3 @@ -146,7 +146,7 @@
     1.4  	| occur (Free _)  = false
     1.5  	| occur (Var (w,_))  = 
     1.6  	    if mem_ix (w, !seen) then false
     1.7 -	    else if v=w then true
     1.8 +	    else if eq_ix(v,w) then true
     1.9  	      (*no need to lookup: v has no assignment*)
    1.10  	    else (seen := w:: !seen;  
    1.11  	          case  Envir.lookup(env,w)  of
    1.12 @@ -209,7 +209,7 @@
    1.13  	| occur (Free _)  = NoOcc
    1.14  	| occur (Var (w,_))  = 
    1.15  	    if mem_ix (w, !seen) then NoOcc
    1.16 -	    else if v=w then Rigid
    1.17 +	    else if eq_ix(v,w) then Rigid
    1.18  	    else (seen := w:: !seen;  
    1.19  	          case  Envir.lookup(env,w)  of
    1.20  		      None    => NoOcc
    1.21 @@ -218,7 +218,7 @@
    1.22  	| occur (t as f$_) =  (*switch to nonrigid search?*)
    1.23  	   (case head_of_in (env,f) of
    1.24  	      Var (w,_) => (*w is not assigned*)
    1.25 -		if v=w then Rigid  
    1.26 +		if eq_ix(v,w) then Rigid  
    1.27  		else  nonrigid t
    1.28  	    | Abs(_,_,body) => nonrigid t (*not in normal form*)
    1.29  	    | _ => occomb t)
    1.30 @@ -593,7 +593,7 @@
    1.31    let val t = Envir.norm_term env t0  and  u = Envir.norm_term env u0
    1.32    in  case  (head_of t, head_of u) of
    1.33        (Var(v,T), Var(w,U)) =>  (*Check for identical variables...*)
    1.34 -	if v=w then		(*...occur check would falsely return true!*)
    1.35 +	if eq_ix(v,w) then     (*...occur check would falsely return true!*)
    1.36  	    if T=U then (env, add_tpair (rbinder, (t,u), tpairs))
    1.37  	    else raise TERM ("add_ffpair: Var name confusion", [t,u])
    1.38  	else if xless(v,w) then (*prefer to update the LARGER variable*)