diff -r 253f04c1e814 -r 5e7b1ae10eb8 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Mon Aug 27 19:29:07 2018 +0200
+++ b/src/Pure/ML/ml_env.ML	Mon Aug 27 20:43:01 2018 +0200
@@ -174,12 +174,13 @@
         Name_Space.define (Context.Theory thy') true (Binding.name env_name, (tables, ops)) envs;
     in envs' end);
 
-fun make_operations SML: operations =
- {read_source = ML_Lex.read_source SML,
-  explode_token = ML_Lex.explode_content_of SML};
+val Isabelle_operations: operations =
+ {read_source = ML_Lex.read_source,
+  explode_token = ML_Lex.check_content_of #> Symbol.explode #> maps (Symbol.esc #> String.explode)};
 
-val Isabelle_operations = make_operations false;
-val SML_operations = make_operations true;
+val SML_operations: operations =
+ {read_source = ML_Lex.read_source_sml,
+  explode_token = ML_Lex.check_content_of #> String.explode};
 
 val _ = Theory.setup (setup Isabelle Isabelle_operations #> setup SML SML_operations);