# HG changeset patch
# User blanchet
# Date 1403093982 -7200
# Node ID 01b68f625550798e3ad4bec86fd502ae78029958
# Parent  fd539459a112ff9f585f569db1679aa791079bb2
automatically learn MaSh facts also in 'blocking' mode

diff -r fd539459a112 -r 01b68f625550 src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jun 18 13:23:09 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_commands.ML	Wed Jun 18 14:19:42 2014 +0200
@@ -52,10 +52,8 @@
 fun del_fact_override ns : fact_override = {add = [], del = ns, only = false}
 fun only_fact_override ns : fact_override = {add = ns, del = [], only = true}
 fun merge_fact_override_pairwise (r1 : fact_override) (r2 : fact_override) =
-  {add = #add r1 @ #add r2, del = #del r1 @ #del r2,
-   only = #only r1 andalso #only r2}
-fun merge_fact_overrides rs =
-  fold merge_fact_override_pairwise rs (only_fact_override [])
+  {add = #add r1 @ #add r2, del = #del r1 @ #del r2, only = #only r1 andalso #only r2}
+fun merge_fact_overrides rs = fold merge_fact_override_pairwise rs (only_fact_override [])
 
 (*** parameters ***)
 
diff -r fd539459a112 -r 01b68f625550 src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Jun 18 13:23:09 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_mash.ML	Wed Jun 18 14:19:42 2014 +0200
@@ -1381,7 +1381,7 @@
 fun flop_wrt_access_graph name =
   Graph.map_node name (fn (_, feats, deps) => (Isar_Proof_wegen_Prover_Flop, feats, deps))
 
-val learn_timeout_slack = 2.0
+val learn_timeout_slack = 20.0
 
 fun launch_thread timeout task =
   let
@@ -1643,7 +1643,7 @@
   else
     let
       fun maybe_launch_thread () =
-        if not blocking andalso not (Async_Manager.has_running_threads MaShN) andalso
+        if not (Async_Manager.has_running_threads MaShN) andalso
            Time.toSeconds timeout >= min_secs_for_learning then
           let val timeout = time_mult learn_timeout_slack timeout in
             launch_thread timeout