# HG changeset patch
# User wenzelm
# Date 1513284043 -3600
# Node ID b8f30228a55b272cacb541f0472b1cfbbb70e12e
# Parent  06c91eac25f238ef31c588d96e229b2bd0410634
minor performance tuning, notably for Library.fold_string etc.;

diff -r 06c91eac25f2 -r b8f30228a55b src/Pure/ML/ml_init.ML
--- a/src/Pure/ML/ml_init.ML	Thu Dec 14 21:31:54 2017 +0100
+++ b/src/Pure/ML/ml_init.ML	Thu Dec 14 21:40:43 2017 +0100
@@ -31,3 +31,11 @@
 
 structure Basic_Exn: BASIC_EXN = Exn;
 open Basic_Exn;
+
+structure String =
+struct
+  open String;
+  fun substring (s, i, n) =
+    if n = 1 then String.str (String.sub (s, i))
+    else String.substring (s, i, n);
+end;