# HG changeset patch
# User wenzelm
# Date 1629714355 -7200
# Node ID 09d4175f473e9210c8200ffc42008693091727df
# Parent  43fe7388458fa2851a3370dba4078185f1955123
tuned;

diff -r 43fe7388458f -r 09d4175f473e src/Pure/General/symbol_explode.ML
--- a/src/Pure/General/symbol_explode.ML	Mon Aug 23 11:40:54 2021 +0200
+++ b/src/Pure/General/symbol_explode.ML	Mon Aug 23 12:25:55 2021 +0200
@@ -18,13 +18,12 @@
 fun explode string =
   let
     fun char i = String.sub (string, i);
-    fun string_range i j = String.substring (string, i, j - i);
+    fun substring i j = String.substring (string, i, j - i);
 
     val n = size string;
     fun test pred i = i < n andalso pred (char i);
     fun many pred i = if test pred i then many pred (i + 1) else i;
-    fun maybe pred i = if test pred i then i + 1 else i;
-    fun maybe_char c = maybe (fn c' => c = c');
+    fun maybe_char c i = if test (fn c' => c = c') i then i + 1 else i;
     fun maybe_ascii_id i = if test is_ascii_letter i then many is_ascii_letdig (i + 1) else i;
 
     fun scan i =
@@ -39,11 +38,11 @@
           (*utf8*)
           else if is_utf8 ch then
             let val j = many is_utf8_trailer (i + 1)
-            in string_range i j :: scan j end
+            in substring i j :: scan j end
           (*named symbol*)
           else if ch = #"\\" andalso test (fn c => c = #"<") (i + 1) then
             let val j = (i + 2) |> maybe_char #"^" |> maybe_ascii_id |> maybe_char #">"
-            in string_range i j :: scan j end
+            in substring i j :: scan j end
           (*single character*)
           else String.str ch :: scan (i + 1)
         end