src/Pure/Thy/thy_output.ML

 (* outer syntax *)
 
 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.$$$ "]")) [];
 
 in

 
 val tag = (improper -- Parse.$$$ "%" -- improper) |-- Parse.!!! (Parse.tag_name --| blank_end);
 
 val locale =
   Scan.option ((Parse.$$$ "(" -- improper -- Parse.$$$ "in") |--
-    Parse.!!! (improper |-- Parse.xname --| (improper -- Parse.$$$ ")")));
+    Parse.!!! (improper |-- Parse.name --| (improper -- Parse.$$$ ")")));
 
 in
 
 fun present_thy thy command_results toks =
   let