src/Pure/Syntax/syntax_ext.ML
changeset 43323 28e71a685c84
parent 42298 d622145603ee
child 43329 84472e198515
--- a/src/Pure/Syntax/syntax_ext.ML	Thu Jun 09 15:37:37 2011 +0200
+++ b/src/Pure/Syntax/syntax_ext.ML	Thu Jun 09 15:38:49 2011 +0200
@@ -241,7 +241,7 @@
           val rangeT = Term.range_type typ handle Match =>
             err_in_mfix "Missing structure argument for indexed syntax" mfix;
 
-          val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
+          val xs = map Ast.Variable (Name.invents Name.context "xa" (length args - 1));
           val (xs1, xs2) = chop (find_index is_index args) xs;
           val i = Ast.Variable "i";
           val lhs = Ast.mk_appl (Ast.Constant indexed_const)