src/Pure/Syntax/syn_ext.ML
changeset 19012 2577ac76cdc6
parent 19004 a72c7a1eb129
child 19046 bc5c6c9b114e
     1.1 --- a/src/Pure/Syntax/syn_ext.ML	Sat Feb 11 17:17:45 2006 +0100
     1.2 +++ b/src/Pure/Syntax/syn_ext.ML	Sat Feb 11 17:17:47 2006 +0100
     1.3 @@ -298,7 +298,7 @@
     1.4              err_in_mfix "Missing structure argument for indexed syntax" mfix;
     1.5  
     1.6            val xs = map Ast.Variable (Term.invent_names [] "xa" (length args - 1));
     1.7 -          val (xs1, xs2) = Library.splitAt (Library.find_index is_index args, xs);
     1.8 +          val (xs1, xs2) = chop (find_index is_index args) xs;
     1.9            val i = Ast.Variable "i";
    1.10            val lhs = Ast.mk_appl (Ast.Constant indexed_const)
    1.11              (xs1 @ [Ast.mk_appl (Ast.Constant "_index") [i]] @ xs2);