# HG changeset patch
# User wenzelm
# Date 1152613028 -7200
# Node ID 717b1eb434f18d9ee1f884c7e1a34ca78bdabd8f
# Parent  b0f5981b926778fa255abb6d3ec80f7f5ffac740
removed obsolete mem_ix;

diff -r b0f5981b9267 -r 717b1eb434f1 src/Pure/unify.ML
--- 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