--- 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 ***)
--- 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