# HG changeset patch
# User wenzelm
# Date 1551091115 -3600
# Node ID 9a7f94ab4df9d2c76c4d26c14cd42e63cb25d513
# Parent  b3c9291b5fc7858aa837391272d2176a8c4b6b78
tuned;

diff -r b3c9291b5fc7 -r 9a7f94ab4df9 src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Sun Feb 24 20:44:17 2019 +0100
+++ b/src/Pure/ML/ml_lex.ML	Mon Feb 25 11:38:35 2019 +0100
@@ -371,10 +371,11 @@
       if Position.is_reported_range pos
       then Position.report pos (language (Input.is_delimited source))
       else ();
-    val syms =
-      Symbol_Pos.explode (Input.text_of source, pos)
-      |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p));
-  in reader {opaque_warning = opaque_warning} scan syms end;
+  in
+    Input.source_explode source
+    |> not symbols ? maps (fn (s, p) => raw_explode s |> map (rpair p))
+    |> reader {opaque_warning = opaque_warning} scan
+  end;
 
 val read_source =
   read_source' {language = Markup.language_ML, symbols = true, opaque_warning = true}