| changeset 69207 | ae2074acbaa8 |
| parent 68028 | 1f9f973eed2a |
| child 69623 | ef02c5e051e5 |
--- a/src/Tools/Code/code_ml.ML Sun Oct 28 16:31:13 2018 +0100 +++ b/src/Tools/Code/code_ml.ML Tue Oct 30 15:45:24 2018 +0100 @@ -55,7 +55,7 @@ if c = "\\" then "\\092" (*produce strings suitable for both SML as well as Isabelle/ML*) else if Symbol.is_ascii c - then ML_Syntax.print_char c + then ML_Syntax.print_symbol_char c else error "non-ASCII byte in SML string literal"; val print_sml_string = quote o translate_string print_sml_char;