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) ~