# HG changeset patch
# User haftmann
# Date 1196860573 -3600
# Node ID 68de88c7e877d85d0a25b37bdb330eb971b4c5b7
# Parent  e209975d56061d29d77a0284a2bd73763f6561f7
added parser for multi_arity

diff -r e209975d5606 -r 68de88c7e877 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Dec 05 14:16:12 2007 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Wed Dec 05 14:16:13 2007 +0100
@@ -56,6 +56,7 @@
   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
@@ -208,6 +209,9 @@
 val arity = xname -- ($$$ "::" |-- !!!
   (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
 
+val multi_arity = and_list1 xname -- ($$$ "::" |-- !!!
+  (Scan.optional ($$$ "(" |-- !!! (list1 sort --| $$$ ")")) [] -- sort)) >> triple2;
+
 
 (* types *)