1.1 --- a/src/Pure/library.ML	Wed Aug 27 12:01:59 2008 +0200
     1.2 +++ b/src/Pure/library.ML	Wed Aug 27 16:32:18 2008 +0200
     1.3 @@ -142,6 +142,7 @@
     1.4    val fold_string: (string -> 'a -> 'a) -> string -> 'a -> 'a
     1.5    val exists_string: (string -> bool) -> string -> bool
     1.6    val forall_string: (string -> bool) -> string -> bool
     1.7 +  val find_substring: string -> string -> int option
     1.8    val enclose: string -> string -> string -> string
     1.9    val unenclose: string -> string
    1.10    val quote: string -> string
    1.11 @@ -731,6 +732,16 @@
    1.12  
    1.13  fun forall_string pred = not o exists_string (not o pred);
    1.14  
    1.15 +fun find_substring s str =
    1.16 +  let
    1.17 +    val n = size s;
    1.18 +    val len = size str;
    1.19 +    fun find i =
    1.20 +      if i + n > len then NONE
    1.21 +      else if String.substring (str, i, n) = s then SOME i
    1.22 +      else find (i + 1);
    1.23 +  in find 0 end;
    1.24 +
    1.25  (*enclose in brackets*)
    1.26  fun enclose lpar rpar str = lpar ^ str ^ rpar;
    1.27  fun unenclose str = String.substring (str, 1, size str - 2);