1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 26 09:23:21 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_util.ML	Thu Aug 26 10:42:06 2010 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  
     1.5  signature SLEDGEHAMMER_UTIL =
     1.6  sig
     1.7 -  val is_true_for : (string * bool) vector -> string -> bool
     1.8 +  val find_first_in_vector : (''a * 'b) vector -> ''a -> 'b -> 'b
     1.9    val plural_s : int -> string
    1.10    val serial_commas : string -> string list -> string list
    1.11    val simplify_spaces : string -> string
    1.12 @@ -29,8 +29,9 @@
    1.13  structure Sledgehammer_Util : SLEDGEHAMMER_UTIL =
    1.14  struct
    1.15  
    1.16 -fun is_true_for v s =
    1.17 -  Vector.foldl (fn ((s', b'), b) => if s' = s then b' else b) false v
    1.18 +fun find_first_in_vector vec key default =
    1.19 +  Vector.foldl (fn ((key', value'), value) =>
    1.20 +                   if key' = key then value' else value) default vec
    1.21  
    1.22  fun plural_s n = if n = 1 then "" else "s"
    1.23