src/Pure/unify.ML

   | occurs (t::ts) =  occur t  orelse  occurs ts
       and occur (Const _)  = false
   | 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;
             case Envir.lookup (env, (w, T)) of
           NONE    => false

         | occomb t = occur t
       and occur (Const _)  = NoOcc
   | 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
           NONE    => NoOcc
         | SOME t => occur t)