src/Pure/Syntax/syntax_ext.ML
changeset 81507 08574da77b4a
parent 81225 2157039256d3
child 81588 81a72b7fcb0c
--- a/src/Pure/Syntax/syntax_ext.ML	Fri Nov 29 11:26:17 2024 +0100
+++ b/src/Pure/Syntax/syntax_ext.ML	Fri Nov 29 17:40:15 2024 +0100
@@ -388,7 +388,7 @@
           val rangeT = Term.range_type typ handle Match =>
             err_in_mixfix "Missing structure argument for indexed syntax";
 
-          val xs = map Ast.Variable (Name.invent Name.context "xa" (length args - 1));
+          val xs = map Ast.Variable (Name.invent_global "xa" (length args - 1));
           val (xs1, xs2) = chop (find_index is_index args) xs;
           val i = Ast.Variable "i";
           val lhs =