src/Pure/Thy/thy_header.ML
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;