src/Pure/variable.ML

--- a/src/Pure/variable.ML	Wed Dec 18 22:26:21 2019 +0100
+++ b/src/Pure/variable.ML	Thu Dec 19 14:46:10 2019 +0100
@@ -429,10 +429,10 @@
       |> declare_constraints (Syntax.free x')
   end;
 
-fun new_fixes names' xs xs' ps =
+fun new_fixes names' args =
   map_names (K names') #>
-  fold new_fixed ((xs ~~ xs') ~~ ps) #>
-  pair xs';
+  fold new_fixed args #>
+  pair (map (#2 o #1) args);
 
 in
 
@@ -452,13 +452,14 @@
     val (xs', names') =
       if is_body ctxt then fold_map Name.variant xs names |>> map Name.skolem
       else (xs, fold Name.declare xs names);
-  in ctxt |> new_fixes names' xs xs' (map Binding.pos_of bs) end;
+  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_of ctxt') (map #1 xs) (map (#1 o dest_Free) xs') no_ps end;
+  in ctxt' |> new_fixes names' ((map #1 xs ~~ map (#1 o dest_Free) xs') ~~ no_ps) end;
 
 fun variant_fixes raw_xs ctxt =
   let
@@ -466,7 +467,7 @@
     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 ctxt |> new_fixes names' ((xs ~~ xs') ~~ no_ps) end;
 
 end;