tuning

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Tue Feb 04 00:04:55 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML	Tue Feb 04 01:03:28 2014 +0100
@@ -41,19 +41,19 @@
       let
         fun mk_step_lfs_gfs lfs gfs = Prove (qs, xs, l, t, subproofs, (lfs, gfs), meths, comment)
 
-        fun minimize_facts _ time min_facts [] = (time, min_facts)
-          | minimize_facts mk_step time min_facts (f :: facts) =
+        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 time min_facts facts
-            | _ => minimize_facts mk_step time (f :: min_facts) facts)
+              Played time' => minimize_facts mk_step min_facts facts time'
+            | _ => minimize_facts mk_step (fact :: min_facts) facts time)
 
-        val (time, min_lfs) = minimize_facts (fn lfs => mk_step_lfs_gfs lfs gfs0) time [] lfs0
-        val (time, min_gfs) = minimize_facts (mk_step_lfs_gfs min_lfs) time [] gfs0
+        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)];
+        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 *))

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Tue Feb 04 00:04:55 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML	Tue Feb 04 01:03:28 2014 +0100
@@ -146,10 +146,8 @@
       (case preplay_isar_step_for_method ctxt timeout meth step of
         outcome as Played _ => SOME (meth, outcome)
       | _ => NONE)
-
-    val meths = proof_methods_of_isar_step step
   in
-    the_list (Par_List.get_some try_method meths)
+    the_list (Par_List.get_some try_method (proof_methods_of_isar_step step))
   end
 
 type isar_preplay_data = (proof_method * play_outcome Lazy.lazy) list Canonical_Label_Tab.table

--- a/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 00:04:55 2014 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML	Tue Feb 04 01:03:28 2014 +0100
@@ -94,8 +94,8 @@
   Method.insert_tac local_facts THEN'
   (case meth of
     Metis_Method (type_enc_opt, lam_trans_opt) =>
-    Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_type_enc]
-      (the_default default_metis_lam_trans lam_trans_opt) ctxt global_facts
+    Metis_Tactic.metis_tac [type_enc_opt |> the_default partial_typesN]
+      (lam_trans_opt |> the_default default_metis_lam_trans) ctxt global_facts
   | SMT_Method => SMT_Solver.smt_tac ctxt global_facts
   | Meson_Method => Meson.meson_tac ctxt global_facts
   | _ =>