src/Pure/unify.ML
changeset 2140 eaa7ab39889d
parent 1505 14f4c55bbe9a
child 2178 acb0afbf61a3
     1.1 --- a/src/Pure/unify.ML	Wed Oct 30 11:20:27 1996 +0100
     1.2 +++ b/src/Pure/unify.ML	Wed Oct 30 11:21:24 1996 +0100
     1.3 @@ -496,7 +496,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 banned  orelse
     1.8 +	  Bound i => (i-lev) mem_int banned  orelse
     1.9  	      	     exists (rigid_bound (lev, banned)) args
    1.10  	| Var _ => false	(*no rigid occurrences here!*)
    1.11  	| Abs (_,_,u) => 
    1.12 @@ -509,7 +509,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 banned  
    1.17 +	    else  if (i-lev) mem_int banned  
    1.18  		  then raise CHANGE_FAIL (**flexible occurrence: give up**)
    1.19  	    else  Bound (i - length (filter (fn j => j < i-lev) banned))
    1.20  	| change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t)
    1.21 @@ -570,7 +570,7 @@
    1.22  fun clean_ffpair ((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 loot  andalso  j mem loou 
    1.26 +            if  j mem_int loot  andalso  j mem_int loou 
    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);