changeset 74887 | 56247fdb8bbb |
parent 74671 | df12779c3ce8 |
child 80307 | 718daea1cf99 |
--- a/src/Pure/Thy/thy_header.ML Mon Dec 06 15:10:15 2021 +0100 +++ b/src/Pure/Thy/thy_header.ML Mon Dec 06 15:34:54 2021 +0100 @@ -147,7 +147,7 @@ val abbrevs = Parse.and_list1 - (Scan.repeat1 Parse.text -- (Parse.$$$ "=" |-- Parse.!!! (Scan.repeat1 Parse.text)) + (Scan.repeat1 Parse.embedded -- (Parse.$$$ "=" |-- Parse.!!! (Scan.repeat1 Parse.embedded)) >> uncurry (map_product pair)) >> flat; val keyword_decls = Parse.and_list1 keyword_decl >> flat;