--- 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;