src/Pure/unify.ML
changeset 2178 acb0afbf61a3
parent 2140 eaa7ab39889d
child 2193 b7e59795c75b
--- a/src/Pure/unify.ML	Tue Nov 12 11:43:16 1996 +0100
+++ b/src/Pure/unify.ML	Tue Nov 12 11:57:10 1996 +0100
@@ -145,7 +145,7 @@
 	| occur (Bound _)  = false
 	| occur (Free _)  = false
 	| occur (Var (w,_))  = 
-	    if w mem !seen then false
+	    if mem_ix (w, !seen) then false
 	    else if v=w then true
 	      (*no need to lookup: v has no assignment*)
 	    else (seen := w:: !seen;  
@@ -208,7 +208,7 @@
 	| occur (Bound _)  = NoOcc
 	| occur (Free _)  = NoOcc
 	| occur (Var (w,_))  = 
-	    if w mem !seen then NoOcc
+	    if mem_ix (w, !seen) then NoOcc
 	    else if v=w then Rigid
 	    else (seen := w:: !seen;  
 	          case  Envir.lookup(env,w)  of