--- a/src/Tools/Code/code_target.ML Mon Dec 06 15:10:15 2021 +0100
+++ b/src/Tools/Code/code_target.ML Mon Dec 06 15:34:54 2021 +0100
@@ -746,7 +746,7 @@
Outer_Syntax.command \<^command_keyword>\<open>code_printing\<close> "declare dedicated printing for code symbols"
(parse_symbol_pragmas (Code_Printer.parse_const_syntax) (Code_Printer.parse_tyco_syntax)
Parse.string (Parse.minus >> K ()) (Parse.minus >> K ())
- (Parse.text -- Scan.optional (\<^keyword>\<open>for\<close> |-- parse_simple_symbols) [])
+ (Parse.embedded -- Scan.optional (\<^keyword>\<open>for\<close> |-- parse_simple_symbols) [])
>> (Toplevel.theory o fold set_printings_cmd));
val _ =