minor performance tuning, notably for Library.fold_string etc.;
authorwenzelm
Thu Dec 14 21:40:43 2017 +0100 (17 months ago)
changeset 67206b8f30228a55b
parent 67205 06c91eac25f2
child 67207 ad538f6c5d2f
minor performance tuning, notably for Library.fold_string etc.;
src/Pure/ML/ml_init.ML
     1.1 --- a/src/Pure/ML/ml_init.ML	Thu Dec 14 21:31:54 2017 +0100
     1.2 +++ b/src/Pure/ML/ml_init.ML	Thu Dec 14 21:40:43 2017 +0100
     1.3 @@ -31,3 +31,11 @@
     1.4  
     1.5  structure Basic_Exn: BASIC_EXN = Exn;
     1.6  open Basic_Exn;
     1.7 +
     1.8 +structure String =
     1.9 +struct
    1.10 +  open String;
    1.11 +  fun substring (s, i, n) =
    1.12 +    if n = 1 then String.str (String.sub (s, i))
    1.13 +    else String.substring (s, i, n);
    1.14 +end;