equal
deleted
inserted
replaced
343 let |
343 let |
344 val declared_outer = is_declared outer; |
344 val declared_outer = is_declared outer; |
345 val fixes_inner = fixes_of inner; |
345 val fixes_inner = fixes_of inner; |
346 val fixes_outer = fixes_of outer; |
346 val fixes_outer = fixes_of outer; |
347 |
347 |
348 val gen_fixes = map #2 ((uncurry take) (length fixes_inner - length fixes_outer, fixes_inner)); |
348 val gen_fixes = map #2 (take (length fixes_inner - length fixes_outer) fixes_inner); |
349 val still_fixed = not o member (op =) gen_fixes; |
349 val still_fixed = not o member (op =) gen_fixes; |
350 |
350 |
351 val type_occs_inner = type_occs_of inner; |
351 val type_occs_inner = type_occs_of inner; |
352 fun gen_fixesT ts = |
352 fun gen_fixesT ts = |
353 Symtab.fold (fn (a, xs) => |
353 Symtab.fold (fn (a, xs) => |