452 val (xs', names') = |
452 val (xs', names') = |
453 if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem |
453 if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem |
454 else (xs, fold Name.declare xs names); |
454 else (xs, fold Name.declare xs names); |
455 in ctxt |> new_fixes names' ((xs ~~ xs') ~~ map Binding.pos_of bs) end; |
455 in ctxt |> new_fixes names' ((xs ~~ xs') ~~ map Binding.pos_of bs) end; |
456 |
456 |
457 fun bound_fixes xs ctxt = |
457 fun variant_names ctxt raw_xs = |
458 let |
|
459 val (xs', ctxt') = fold_map next_bound xs ctxt; |
|
460 val names' = names_of ctxt'; |
|
461 val no_ps = replicate (length xs) Position.none; |
|
462 in ctxt' |> new_fixes names' ((map #1 xs ~~ map (#1 o dest_Free) xs') ~~ no_ps) end; |
|
463 |
|
464 fun variant_fixes raw_xs ctxt = |
|
465 let |
458 let |
466 val names = names_of ctxt; |
459 val names = names_of ctxt; |
467 val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs; |
460 val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs; |
468 val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem); |
461 val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem); |
469 val no_ps = replicate (length xs) Position.none; |
462 in (names', xs ~~ xs') end; |
470 in ctxt |> new_fixes names' ((xs ~~ xs') ~~ no_ps) end; |
463 |
|
464 fun variant_fixes xs ctxt = |
|
465 let val (names', vs) = variant_names ctxt xs; |
|
466 in ctxt |> new_fixes names' (map (rpair Position.none) vs) end; |
|
467 |
|
468 fun bound_fixes xs ctxt = |
|
469 let |
|
470 val (names', vs) = variant_names ctxt (map #1 xs); |
|
471 val (ys, ctxt') = fold_map next_bound (map2 (fn (x', _) => fn (_, T) => (x', T)) vs xs) ctxt; |
|
472 val fixes = map2 (fn (x, _) => fn Free (y, _) => ((x, y), Position.none)) vs ys; |
|
473 in ctxt' |> new_fixes names' fixes end; |
471 |
474 |
472 end; |
475 end; |
473 |
476 |
474 val add_fixes = add_fixes_binding o map Binding.name; |
477 val add_fixes = add_fixes_binding o map Binding.name; |
475 |
478 |