src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML

 val auto = Unsynchronized.ref false
 
 val _ =
   ProofGeneralPgip.add_preference Preferences.category_tracing
       (Preferences.bool_pref auto "auto-sledgehammer"
-           "Whether to run Sledgehammer automatically.")
+           "Run Sledgehammer automatically.")
 
 (** Sledgehammer commands **)
 
 val no_relevance_override = {add = [], del = [], only = false}
 fun add_relevance_override ns : relevance_override =

     fun general_lookup_bool option default_value name =
       case lookup name of
         SOME s => parse_bool_option option name s
       | NONE => default_value
     val lookup_bool = the o general_lookup_bool false (SOME false)
-    val lookup_bool_option = general_lookup_bool true NONE
     fun lookup_time name =
       case lookup name of
         SOME s => parse_time_option name s
       | NONE => NONE
     fun lookup_int name =