src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
changeset 39573 61547eda78b4
parent 39570 05452dd66b2b
child 39581 87a9ff4d5817
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Sep 11 12:31:05 2010 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Sat Sep 11 12:31:42 2010 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4  val _ =
     1.5    ProofGeneralPgip.add_preference Preferences.category_tracing
     1.6        (Preferences.bool_pref auto "auto-sledgehammer"
     1.7 -           "Whether to run Sledgehammer automatically.")
     1.8 +           "Run Sledgehammer automatically.")
     1.9  
    1.10  (** Sledgehammer commands **)
    1.11  
    1.12 @@ -153,7 +153,6 @@
    1.13          SOME s => parse_bool_option option name s
    1.14        | NONE => default_value
    1.15      val lookup_bool = the o general_lookup_bool false (SOME false)
    1.16 -    val lookup_bool_option = general_lookup_bool true NONE
    1.17      fun lookup_time name =
    1.18        case lookup name of
    1.19          SOME s => parse_time_option name s