# HG changeset patch
# User smolkas
# Date 1374096993 -7200
# Node ID 9306c309b892cb7a68190618e074b399ba73878f
# Parent  f06b403a7dcdb54c1c951e9213fdfce9db7c8ddb
tuned

diff -r f06b403a7dcd -r 9306c309b892 src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Wed Jul 17 21:48:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_compress.ML	Wed Jul 17 23:36:33 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 f06b403a7dcd -r 9306c309b892 src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Wed Jul 17 21:48:21 2013 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_preplay.ML	Wed Jul 17 23:36:33 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