equal
deleted
inserted
replaced
471 fun change_bnos banned = |
471 fun change_bnos banned = |
472 let fun change lev (Bound i) = |
472 let fun change lev (Bound i) = |
473 if i<lev then Bound i |
473 if i<lev then Bound i |
474 else if member (op =) banned (i-lev) |
474 else if member (op =) banned (i-lev) |
475 then raise CHANGE_FAIL (**flexible occurrence: give up**) |
475 then raise CHANGE_FAIL (**flexible occurrence: give up**) |
476 else Bound (i - length (List.filter (fn j => j < i-lev) banned)) |
476 else Bound (i - length (filter (fn j => j < i-lev) banned)) |
477 | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) |
477 | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) |
478 | change lev (t$u) = change lev t $ change lev u |
478 | change lev (t$u) = change lev t $ change lev u |
479 | change lev t = t |
479 | change lev t = t |
480 in change 0 end; |
480 in change 0 end; |
481 |
481 |