# HG changeset patch
# User wenzelm
# Date 1576765355 -3600
# Node ID e58bc223f46c225040e8a4830107123cfb6e3a26
# Parent  3fc2def62547b7835108f31beb7d4f013aab574a
more robust bound_fixes: external name does appear in "fixes" name space and could clash with direct fixes (e.g. via Subgoal.FOCUS within a global context);

diff -r 3fc2def62547 -r e58bc223f46c src/Pure/variable.ML
--- 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;