--- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Thu Apr 15 13:57:17 2010 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML Fri Apr 16 14:48:34 2010 +0200
@@ -8,6 +8,8 @@
sig
val plural_s : int -> string
val serial_commas : string -> string list -> string list
+ val replace_all : string -> string -> string -> string
+ val remove_all : string -> string -> string
val parse_bool_option : bool -> string -> string -> bool option
val parse_time_option : string -> string -> Time.time option
val hashw : word * word -> word
@@ -26,6 +28,18 @@
| serial_commas conj [s1, s2, s3] = [s1 ^ ",", s2 ^ ",", conj, s3]
| serial_commas conj (s :: ss) = s ^ "," :: serial_commas conj ss
+fun replace_all bef aft =
+ let
+ fun aux seen "" = String.implode (rev seen)
+ | aux seen s =
+ if String.isPrefix bef s then
+ aux seen "" ^ aft ^ aux [] (unprefix bef s)
+ else
+ aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
+ in aux [] end
+
+fun remove_all bef = replace_all bef ""
+
fun parse_bool_option option name s =
(case s of
"smart" => if option then NONE else raise Option