--- a/src/Pure/Thy/thy_output.ML Wed Apr 13 17:00:02 2016 +0200
+++ b/src/Pure/Thy/thy_output.ML Wed Apr 13 18:01:05 2016 +0200
@@ -143,7 +143,7 @@
local
val property =
- Parse.position Parse.xname -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.xname) "";
+ Parse.position Parse.name -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
val properties =
Scan.optional (Parse.$$$ "[" |-- Parse.!!! (Parse.enum "," property --| Parse.$$$ "]")) [];
@@ -404,7 +404,7 @@
val locale =
Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
- Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
+ Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
in