src/Pure/unify.ML
changeset 20083 717b1eb434f1
parent 20020 9e7d3d06c643
child 20098 19871ee094b1
--- 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