silence methods even better
authorblanchet
Fri May 16 19:13:50 2014 +0200 (2014-05-16)
changeset 5698251d4189d95cf
parent 56981 3ef45ce002b5
child 56983 132142089ea6
silence methods even better
src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
src/HOL/Tools/try0.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri May 16 19:13:50 2014 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Fri May 16 19:13:50 2014 +0200
     1.3 @@ -279,8 +279,7 @@
     1.4      val overlord = lookup_bool "overlord"
     1.5      val spy = getenv "SLEDGEHAMMER_SPY" = "yes" orelse lookup_bool "spy"
     1.6      val blocking =
     1.7 -      Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse
     1.8 -      lookup_bool "blocking"
     1.9 +      Isabelle_Process.is_active () orelse mode <> Normal orelse debug orelse lookup_bool "blocking"
    1.10      val provers = lookup_string "provers" |> space_explode " "
    1.11                    |> mode = Auto_Try ? single o hd
    1.12      val type_enc =
    1.13 @@ -360,7 +359,8 @@
    1.14  
    1.15  fun hammer_away override_params subcommand opt_i fact_override state0 =
    1.16    let
    1.17 -    val state = Proof.map_context (Try0.silence_methods false) state0
    1.18 +    val state =
    1.19 +      Proof.map_contexts (Try0.silence_methods false #> Config.put SMT2_Config.verbose false) state0
    1.20      val thy = Proof.theory_of state
    1.21      val ctxt = Proof.context_of state
    1.22  
     2.1 --- a/src/HOL/Tools/try0.ML	Fri May 16 19:13:50 2014 +0200
     2.2 +++ b/src/HOL/Tools/try0.ML	Fri May 16 19:13:50 2014 +0200
     2.3 @@ -122,7 +122,7 @@
     2.4  
     2.5  fun generic_try0 mode timeout_opt quad st =
     2.6    let
     2.7 -    val st = st |> Proof.map_context (silence_methods false);
     2.8 +    val st = Proof.map_contexts (silence_methods false) st;
     2.9      fun trd (_, _, t) = t;
    2.10      fun par_map f =
    2.11        if mode = Normal then Par_List.map f #> map_filter I #> sort (int_ord o pairself trd)