--- a/src/Pure/unify.ML Tue Jul 11 12:17:07 2006 +0200
+++ b/src/Pure/unify.ML Tue Jul 11 12:17:08 2006 +0200
@@ -87,7 +87,7 @@
| occur (Bound _) = false
| occur (Free _) = false
| occur (Var (w, T)) =
- if mem_ix (w, !seen) then false
+ if member (op =) (!seen) w then false
else if eq_ix(v,w) then true
(*no need to lookup: v has no assignment*)
else (seen := w:: !seen;
@@ -150,7 +150,7 @@
| occur (Bound _) = NoOcc
| occur (Free _) = NoOcc
| occur (Var (w, T)) =
- if mem_ix (w, !seen) then NoOcc
+ if member (op =) (!seen) w then NoOcc
else if eq_ix(v,w) then Rigid
else (seen := w:: !seen;
case Envir.lookup (env, (w, T)) of