src/Pure/Syntax/syn_ext.ML
changeset 20076 def4ad161528
parent 19482 9f11af8f7ef9
child 20675 cb19d18aef01
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Tue Jul 11 12:17:00 2006 +0200
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Tue Jul 11 12:17:01 2006 +0200
     1.3 @@ -297,7 +297,7 @@
     1.4            val rangeT = Term.range_type typ handle Match =>
     1.5              err_in_mfix "Missing structure argument for indexed syntax" mfix;
     1.6  
     1.7 -          val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
     1.8 +          val xs = map Ast.Variable (Name.invent_list [] "xa" (length args - 1));
     1.9            val (xs1, xs2) = chop (find_index is_index args) xs;
    1.10            val i = Ast.Variable "i";
    1.11            val lhs = Ast.mk_appl (Ast.Constant indexed_const)