diff -r f0a8d882c031 -r 23df00d48d6f src/Tools/Code/code_target.ML --- a/src/Tools/Code/code_target.ML Sun Mar 30 11:21:32 2025 +0200 +++ b/src/Tools/Code/code_target.ML Sun Mar 30 11:21:34 2025 +0200 @@ -762,8 +762,8 @@ val _ = Outer_Syntax.command \<^command_keyword>\code_printing\ "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.embedded -- Scan.optional (\<^keyword>\for\ |-- parse_simple_symbols) []) + Code_Printer.parse_target_source (Parse.minus >> K ()) (Parse.minus >> K ()) + (Code_Printer.parse_target_source -- Scan.optional (\<^keyword>\for\ |-- parse_simple_symbols) []) >> (Toplevel.theory o fold set_printings_cmd)); val _ =