src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
changeset 36169 27b1cc58715e
parent 36142 f5e15e9aae10
child 36170 0cdb76723c88
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Apr 15 13:57:17 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Fri Apr 16 14:48:34 2010 +0200
     1.3 @@ -8,6 +8,8 @@
     1.4  sig
     1.5    val plural_s : int -> string
     1.6    val serial_commas : string -> string list -> string list
     1.7 +  val replace_all : string -> string -> string -> string
     1.8 +  val remove_all : string -> string -> string
     1.9    val parse_bool_option : bool -> string -> string -> bool option
    1.10    val parse_time_option : string -> string -> Time.time option
    1.11    val hashw : word * word -> word
    1.12 @@ -26,6 +28,18 @@
    1.13    | serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
    1.14    | serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
    1.15  
    1.16 +fun replace_all bef aft =
    1.17 +  let
    1.18 +    fun aux seen "" = String.implode (rev seen)
    1.19 +      | aux seen s =
    1.20 +      if String.isPrefix bef s then
    1.21 +          aux seen "" ^ aft ^ aux [] (unprefix bef s)
    1.22 +        else
    1.23 +          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
    1.24 +  in aux [] end
    1.25 +
    1.26 +fun remove_all bef = replace_all bef ""
    1.27 +
    1.28  fun parse_bool_option option name s =
    1.29    (case s of
    1.30       "smart" => if option then NONE else raise Option