src/Pure/Syntax/syntax_ext.ML

             if const <> "" then const ^ "_indexed"
             else err_in_mfix "Missing constant name for indexed syntax" mfix;
           val rangeT = Term.range_type typ handle Match =>
             err_in_mfix "Missing structure argument for indexed syntax" mfix;
 
-          val xs = map Ast.Variable (Name.invents Name.context "xa" (length args - 1));
+          val xs = map Ast.Variable (Name.invent 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)
             (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);
           val rhs = Ast.mk_appl (Ast.Constant const) (i :: xs);