src/Pure/Syntax/syn_ext.ML

--- a/src/Pure/Syntax/syn_ext.ML	Tue Jul 11 12:17:00 2006 +0200
+++ b/src/Pure/Syntax/syn_ext.ML	Tue Jul 11 12:17:01 2006 +0200
@@ -297,7 +297,7 @@
           val rangeT = Term.range_type typ handle Match =>
             err_in_mfix "Missing structure argument for indexed syntax" mfix;
 
-          val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
+          val xs = map Ast.Variable (Name.invent_list [] "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)