# HG changeset patch
# User blanchet
# Date 1406897037 -7200
# Node ID d99080b7f961373ba76bb9653e4a1d4cd4eb9b7c
# Parent  d39815cdb7ba6230f97316e6091d5d4bc5f3b0d1
tuning

diff -r d39815cdb7ba -r d99080b7f961 src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Fri Aug 01 14:43:57 2014 +0200
@@ -35,28 +35,32 @@
 
 val slack = seconds 0.025
 
+fun minimized_isar_step ctxt time
+    (Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) =
+  let
+    val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00
+
+    fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
+
+    fun minimize_facts _ min_facts [] time = (min_facts, time)
+      | minimize_facts mk_step min_facts (fact :: facts) time =
+        (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth
+            (mk_step (min_facts @ facts)) of
+          Played time' => minimize_facts mk_step min_facts facts time'
+        | _ => minimize_facts mk_step (fact :: min_facts) facts time)
+
+    val (min_lfs, time') = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time
+    val (min_gfs, time'') = minimize_facts (mk_step_lfs_gfs min_lfs) [] gfs0 time'
+  in
+    (time'', mk_step_lfs_gfs min_lfs min_gfs)
+  end
+
 fun minimize_isar_step_dependencies ctxt preplay_data
-      (step as Prove (qs, xs, l, t, subproofs, (lfs0, gfs00), meths as meth :: _, comment)) =
+      (step as Prove (_, _, l, _, _, _, meth :: _, _)) =
     (case Lazy.force (preplay_outcome_of_isar_step_for_method (!preplay_data) l meth) of
       Played time =>
-      let
-        val gfs0 = filter (thms_influence_proof_method ctxt meth o thms_of_name ctxt) gfs00
-
-        fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
-
-        fun minimize_facts _ min_facts [] time = (min_facts, time)
-          | minimize_facts mk_step min_facts (fact :: facts) time =
-            (case preplay_isar_step_for_method ctxt (Time.+ (time, slack)) meth
-                (mk_step (min_facts @ facts)) of
-              Played time' => minimize_facts mk_step min_facts facts time'
-            | _ => minimize_facts mk_step (fact :: min_facts) facts time)
-
-        val (min_lfs, time') = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) [] lfs0 time
-        val (min_gfs, time'') = minimize_facts (mk_step_lfs_gfs min_lfs) [] gfs0 time'
-
-        val step' = mk_step_lfs_gfs min_lfs min_gfs
-      in
-        set_preplay_outcomes_of_isar_step ctxt time'' preplay_data step' [(meth, Played time'')];
+      let val (time', step') = minimized_isar_step ctxt time step in
+        set_preplay_outcomes_of_isar_step ctxt time' preplay_data step' [(meth, Played time')];
         step'
       end
     | _ => step (* don't touch steps that time out or fail *))