--- a/src/Pure/variable.ML Thu Dec 19 14:46:10 2019 +0100
+++ b/src/Pure/variable.ML Thu Dec 19 15:22:35 2019 +0100
@@ -454,20 +454,23 @@
else (xs, fold Name.declare xs names);
in ctxt |> new_fixes names' ((xs ~~ xs') ~~ map Binding.pos_of bs) end;
-fun bound_fixes xs ctxt =
- let
- val (xs', ctxt') = fold_map next_bound xs ctxt;
- val names' = names_of ctxt';
- val no_ps = replicate (length xs) Position.none;
- in ctxt' |> new_fixes names' ((map #1 xs ~~ map (#1 o dest_Free) xs') ~~ no_ps) end;
-
-fun variant_fixes raw_xs ctxt =
+fun variant_names ctxt raw_xs =
let
val names = names_of ctxt;
val xs = map (fn x => Name.clean x |> Name.is_internal x ? Name.internal) raw_xs;
val (xs', names') = fold_map Name.variant xs names |>> (is_body ctxt ? map Name.skolem);
- val no_ps = replicate (length xs) Position.none;
- in ctxt |> new_fixes names' ((xs ~~ xs') ~~ no_ps) end;
+ in (names', xs ~~ xs') end;
+
+fun variant_fixes xs ctxt =
+ let val (names', vs) = variant_names ctxt xs;
+ in ctxt |> new_fixes names' (map (rpair Position.none) vs) end;
+
+fun bound_fixes xs ctxt =
+ let
+ val (names', vs) = variant_names ctxt (map #1 xs);
+ val (ys, ctxt') = fold_map next_bound (map2 (fn (x', _) => fn (_, T) => (x', T)) vs xs) ctxt;
+ val fixes = map2 (fn (x, _) => fn Free (y, _) => ((x, y), Position.none)) vs ys;
+ in ctxt' |> new_fixes names' fixes end;
end;