src/Pure/unify.ML
changeset 20664 ffbc5a57191a
parent 20548 8ef25fe585a8
child 23178 07ba6b58b3d2
     1.1 --- a/src/Pure/unify.ML	Thu Sep 21 19:04:12 2006 +0200
     1.2 +++ b/src/Pure/unify.ML	Thu Sep 21 19:04:20 2006 +0200
     1.3 @@ -426,7 +426,7 @@
     1.4    let val (head,args) = strip_comb t
     1.5    in
     1.6        case head of
     1.7 -    Bound i => (i-lev) mem_int banned  orelse
     1.8 +    Bound i => member (op =) banned (i-lev)  orelse
     1.9                 exists (rigid_bound (lev, banned)) args
    1.10    | Var _ => false  (*no rigid occurrences here!*)
    1.11    | Abs (_,_,u) =>
    1.12 @@ -439,7 +439,7 @@
    1.13  fun change_bnos banned =
    1.14    let fun change lev (Bound i) =
    1.15        if i<lev then Bound i
    1.16 -      else  if (i-lev) mem_int banned
    1.17 +      else  if member (op =) banned (i-lev)
    1.18        then raise CHANGE_FAIL (**flexible occurrence: give up**)
    1.19        else  Bound (i - length (List.filter (fn j => j < i-lev) banned))
    1.20    | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
    1.21 @@ -500,7 +500,7 @@
    1.22  fun clean_ffpair thy ((rbinder, t, u), (env,tpairs)) =
    1.23    let val loot = loose_bnos t  and  loou = loose_bnos u
    1.24        fun add_index (((a,T), j), (bnos, newbinder)) =
    1.25 -            if  j mem_int loot  andalso  j mem_int loou
    1.26 +            if  member (op =) loot j  andalso  member (op =) loou j
    1.27              then  (bnos, (a,T)::newbinder)  (*needed by both: keep*)
    1.28              else  (j::bnos, newbinder);   (*remove*)
    1.29        val indices = 0 upto (length rbinder - 1);