changeset 33317 | b4534348b8fd |
parent 33063 | 4d462963a7db |
child 35408 | b48ab741683b |
--- a/src/Pure/unify.ML Thu Oct 29 16:59:12 2009 +0100 +++ b/src/Pure/unify.ML Thu Oct 29 17:58:26 2009 +0100 @@ -473,7 +473,7 @@ if i<lev then Bound i else if member (op =) banned (i-lev) then raise CHANGE_FAIL (**flexible occurrence: give up**) - else Bound (i - length (List.filter (fn j => j < i-lev) banned)) + else Bound (i - length (filter (fn j => j < i-lev) banned)) | change lev (Abs (a,T,t)) = Abs (a, T, change(lev+1) t) | change lev (t$u) = change lev t $ change lev u | change lev t = t