diff -r 0a6ed065683d -r 27b1cc58715e src/HOL/Tools/Sledgehammer/sledgehammer_util.ML
--- 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