tuning

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_compress.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -155,11 +155,10 @@
             (sub as Proof (_, assms, sub_steps)) :: subs =>
             (let
               (* trivial subproofs have exactly one "Prove" step *)
-              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), meth' :: _))) =
-                try the_single sub_steps
+              val SOME (Prove (_, [], l', _, [], ((lfs', gfs'), _))) = try the_single sub_steps
 
               (* only touch proofs that can be preplayed sucessfully *)
-              val Played time' = forced_preplay_outcome_of_isar_step (!preplay_data) l'
+              val Played time' = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l'
 
               (* merge steps *)
               val subs'' = subs @ nontriv_subs
@@ -181,12 +180,11 @@
           | _ => raise Fail "Sledgehammer_Isar_Compress: elim_one_subproof")
 
       fun elim_subproofs (step as Let _) = step
-        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs,
-            ((lfs, gfs), meths as meth :: _))) =
+        | elim_subproofs (step as Prove (qs, fix, l, t, subproofs, ((lfs, gfs), meths))) =
           if subproofs = [] then
             step
           else
-            (case forced_preplay_outcome_of_isar_step (!preplay_data) l of
+            (case forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l of
               Played time => elim_one_subproof time qs fix l t lfs gfs meths subproofs []
             | _ => step)
 
@@ -220,18 +218,18 @@
 
           fun try_eliminate (i, l, _) labels steps =
             let
-              val ((cand as Prove (_, _, l, _, _, ((lfs, _), meth :: _))) :: steps') = drop i steps
+              val ((cand as Prove (_, _, _, _, _, ((lfs, _), _))) :: steps') = drop i steps
 
               val succs = collect_successors steps' labels
               val succ_meths = map (hd o snd o the o byline_of_isar_step) succs
 
               (* only touch steps that can be preplayed successfully *)
-              val Played time = forced_preplay_outcome_of_isar_step (!preplay_data) l
+              val Played time = forced_intermediate_preplay_outcome_of_isar_step (!preplay_data) l
 
               val succs' = map (try_merge cand #> the) succs
 
               val times0 = map ((fn Played time => time) o
-                forced_preplay_outcome_of_isar_step (!preplay_data)) labels
+                forced_intermediate_preplay_outcome_of_isar_step (!preplay_data)) labels
               val time_slice = time_mult (1.0 / (Real.fromInt (length labels))) time
               val timeouts = map (curry Time.+ time_slice #> slackify_merge_timeout) times0
 

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Mon Feb 03 10:14:18 2014 +0100
@@ -22,7 +22,7 @@
   val set_preplay_outcomes_of_isar_step : Proof.context -> Time.time ->
     isar_preplay_data Unsynchronized.ref -> isar_step ->
     (proof_method * play_outcome Lazy.lazy) list -> unit
-  val forced_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
+  val forced_intermediate_preplay_outcome_of_isar_step : isar_preplay_data -> label -> play_outcome
   val preplay_outcome_of_isar_step_for_method : isar_preplay_data -> label -> proof_method ->
     play_outcome Lazy.lazy
   val fastest_method_of_isar_step : isar_preplay_data -> label -> proof_method
@@ -184,9 +184,7 @@
 
 fun peek_at_outcome outcome = if Lazy.is_finished outcome then Lazy.force outcome else Not_Played
 
-(*
-*)
-fun forced_preplay_outcome_of_isar_step preplay_data l =
+fun forced_intermediate_preplay_outcome_of_isar_step preplay_data l =
   let
     fun get_best_outcome_available get_one =
       the (Canonical_Label_Tab.lookup preplay_data l)