--- 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