# HG changeset patch
# User wenzelm
# Date 1374097870 -7200
# Node ID b24d11ab44ff1095dfadaae0ceac66f346af6861
# Parent  9306c309b892cb7a68190618e074b399ba73878f# Parent  da646aa4a3bbd21e7fa52b20ad84f9bde8501a53
merged

diff -r da646aa4a3bb -r b24d11ab44ff src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- 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')
 
diff -r da646aa4a3bb -r b24d11ab44ff src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- 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