src/Pure/Isar/outer_parse.ML

   val text: token list -> string * token list
   val path: token list -> Path.T * token list
   val parname: token list -> string * token list
   val sort: token list -> string * token list
   val arity: token list -> (string * string list * string) * token list
+  val multi_arity: token list -> (string list * string list * string) * token list
   val type_args: token list -> string list * token list
   val typ: token list -> string * token list
   val mixfix: token list -> mixfix * token list
   val mixfix': token list -> mixfix * token list
   val opt_infix: token list -> mixfix * token list

 val sort = group "sort" xname;
 
 val arity = xname -- ($$$ "::" |-- !!!
   (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
 
+val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
+  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
+
 
 (* types *)
 
 val typ = group "type"
   (short_ident || long_ident || sym_ident || type_ident || type_var || string || number);