--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed Jul 17 23:33:16 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML Wed Jul 17 23:51:10 2013 +0200
@@ -284,6 +284,8 @@
val succs = collect_successors steps' succ_lbls
val succs' = map (try_merge cand #> the) succs
+ (* TODO: should be lazy: stop preplaying as soon as one step
+ fails/times out *)
val preplay_times =
map (uncurry preplay_quietly) (timeouts ~~ succs')
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Jul 17 23:33:16 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML Wed Jul 17 23:51:10 2013 +0200
@@ -160,6 +160,7 @@
val facts =
map (thm_of_proof ctxt) subproofs @ resolve_fact_names ctxt fact_names
val ctxt = ctxt |> Config.put Metis_Tactic.verbose debug
+ |> Config.put Lin_Arith.verbose debug
|> obtain ? Config.put Metis_Tactic.new_skolem true
val goal =
Goal.prove (Config.put Metis_Tactic.verbose debug ctxt) [] [] prop