removed obsolete mem_ix;
authorwenzelm
Tue Jul 11 12:17:08 2006 +0200 (2006-07-11)
changeset 20083717b1eb434f1
parent 20082 b0f5981b9267
child 20084 aa320957f00c
removed obsolete mem_ix;
src/Pure/unify.ML
     1.1 --- a/src/Pure/unify.ML	Tue Jul 11 12:17:07 2006 +0200
     1.2 +++ b/src/Pure/unify.ML	Tue Jul 11 12:17:08 2006 +0200
     1.3 @@ -87,7 +87,7 @@
     1.4    | occur (Bound _)  = false
     1.5    | occur (Free _)  = false
     1.6    | occur (Var (w, T))  =
     1.7 -      if mem_ix (w, !seen) then false
     1.8 +      if member (op =) (!seen) w then false
     1.9        else if eq_ix(v,w) then true
    1.10          (*no need to lookup: v has no assignment*)
    1.11        else (seen := w:: !seen;
    1.12 @@ -150,7 +150,7 @@
    1.13    | occur (Bound _)  = NoOcc
    1.14    | occur (Free _)  = NoOcc
    1.15    | occur (Var (w, T))  =
    1.16 -      if mem_ix (w, !seen) then NoOcc
    1.17 +      if member (op =) (!seen) w then NoOcc
    1.18        else if eq_ix(v,w) then Rigid
    1.19        else (seen := w:: !seen;
    1.20              case Envir.lookup (env, (w, T)) of