# HG changeset patch
# User wenzelm
# Date 1519582592 -3600
# Node ID 012f1e8a12095e7969dceb8d5fb12e63d13e095c
# Parent  5348bea4accdc357f1248e62ea4331c0392f7e60
allow multiple entries of and_list (on both sides);

diff -r 5348bea4accd -r 012f1e8a1209 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Sun Feb 25 15:44:46 2018 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Sun Feb 25 19:16:32 2018 +0100
@@ -66,7 +66,7 @@
     ;
     keyword_decls: (@{syntax string} +) ('::' @{syntax name} @{syntax tags})?
     ;
-    abbrevs: @'abbrevs' ((text '=' text) + @'and')
+    abbrevs: @'abbrevs' (((text+) '=' (text+)) + @'and')
     ;
     @@{command thy_deps} (thy_bounds thy_bounds?)?
     ;
diff -r 5348bea4accd -r 012f1e8a1209 src/Pure/Thy/thy_header.ML
--- a/src/Pure/Thy/thy_header.ML	Sun Feb 25 15:44:46 2018 +0100
+++ b/src/Pure/Thy/thy_header.ML	Sun Feb 25 19:16:32 2018 +0100
@@ -144,7 +144,10 @@
   Scan.optional (Parse.$$$ "::" |-- Parse.!!! keyword_spec) Keyword.no_spec
   >> (fn (names, spec) => map (rpair spec) names);
 
-val abbrevs = Parse.and_list1 (Parse.text -- (Parse.$$$ "=" |-- Parse.!!! Parse.text));
+val abbrevs =
+  Parse.and_list1
+    (Scan.repeat1 Parse.text -- (Parse.$$$ "=" |-- Parse.!!! (Scan.repeat1 Parse.text))
+      >> uncurry (map_product pair)) >> flat;
 
 val keyword_decls = Parse.and_list1 keyword_decl >> flat;
 
diff -r 5348bea4accd -r 012f1e8a1209 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Sun Feb 25 15:44:46 2018 +0100
+++ b/src/Pure/Thy/thy_header.scala	Sun Feb 25 19:16:32 2018 +0100
@@ -138,7 +138,8 @@
       { case xs ~ yss => (xs :: yss).flatten }
 
     val abbrevs =
-      rep1sep(text ~ ($$$("=") ~! text) ^^ { case a ~ (_ ~ b) => (a, b) }, $$$("and"))
+      rep1sep(rep1(text) ~ ($$$("=") ~! rep1(text)), $$$("and")) ^^
+        { case res => for ((as ~ (_ ~ bs)) <- res; a <- as; b <- bs) yield (a, b) }
 
     val args =
       position(theory_name) ~