minor performance tuning, notably for Library.fold_string etc.;

--- 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;