use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
authorblanchet
Tue Oct 15 15:31:18 2013 +0200 (2013-10-15 ago)
changeset 54113df080dfefddc
parent 54112 9c0f464d1854
child 54114 84791e3fdcde
use MePo with Auto Sledgehammer, because it's lighter than MaSh and always available
src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 15 15:26:58 2013 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML	Tue Oct 15 15:31:18 2013 +0200
     1.3 @@ -281,7 +281,9 @@
     1.4      val lam_trans = lookup_option lookup_string "lam_trans"
     1.5      val uncurried_aliases = lookup_option lookup_bool "uncurried_aliases"
     1.6      val learn = lookup_bool "learn"
     1.7 -    val fact_filter = lookup_option lookup_string "fact_filter"
     1.8 +    val fact_filter =
     1.9 +      lookup_option lookup_string "fact_filter"
    1.10 +      |> mode = Auto_Try ? (fn NONE => SOME mepoN | sf => sf)
    1.11      val max_facts = lookup_option lookup_int "max_facts"
    1.12      val fact_thresholds = lookup_real_pair "fact_thresholds"
    1.13      val max_mono_iters = lookup_option lookup_int "max_mono_iters"
    1.14 @@ -291,12 +293,10 @@
    1.15      val isar_compress = Real.max (1.0, lookup_real "isar_compress")
    1.16      val isar_try0 = lookup_bool "isar_try0"
    1.17      val slice = mode <> Auto_Try andalso lookup_bool "slice"
    1.18 -    val minimize =
    1.19 -      if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
    1.20 +    val minimize = if mode = Auto_Try then NONE else lookup_option lookup_bool "minimize"
    1.21      val timeout = if mode = Auto_Try then NONE else lookup_time "timeout"
    1.22      val preplay_timeout =
    1.23 -      if mode = Auto_Try then SOME Time.zeroTime
    1.24 -      else lookup_time "preplay_timeout"
    1.25 +      if mode = Auto_Try then SOME Time.zeroTime else lookup_time "preplay_timeout"
    1.26      val expect = lookup_string "expect"
    1.27    in
    1.28      {debug = debug, verbose = verbose, overlord = overlord, spy = spy, blocking = blocking,