--- 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)