changeset 67722 | 012f1e8a1209 |
parent 67290 | 98b6cd12f963 |
child 68841 | 252b43600737 |
--- 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) ~