src/Pure/unify.ML
changeset 2178 acb0afbf61a3
parent 2140 eaa7ab39889d
child 2193 b7e59795c75b
     1.1 --- a/src/Pure/unify.ML	Tue Nov 12 11:43:16 1996 +0100
     1.2 +++ b/src/Pure/unify.ML	Tue Nov 12 11:57:10 1996 +0100
     1.3 @@ -145,7 +145,7 @@
     1.4  	| occur (Bound _)  = false
     1.5  	| occur (Free _)  = false
     1.6  	| occur (Var (w,_))  = 
     1.7 -	    if w mem !seen then false
     1.8 +	    if mem_ix (w, !seen) then false
     1.9  	    else if v=w then true
    1.10  	      (*no need to lookup: v has no assignment*)
    1.11  	    else (seen := w:: !seen;  
    1.12 @@ -208,7 +208,7 @@
    1.13  	| occur (Bound _)  = NoOcc
    1.14  	| occur (Free _)  = NoOcc
    1.15  	| occur (Var (w,_))  = 
    1.16 -	    if w mem !seen then NoOcc
    1.17 +	    if mem_ix (w, !seen) then NoOcc
    1.18  	    else if v=w then Rigid
    1.19  	    else (seen := w:: !seen;  
    1.20  	          case  Envir.lookup(env,w)  of