# HG changeset patch # User blanchet # Date 1391472208 -3600 # Node ID e0233567a8ef6b357206eacfe936a1e75f1d65ee # Parent cddd94fb0e8de8ba26ebe23075c694722285cf7d tuning diff -r cddd94fb0e8d -r e0233567a8ef src/HOL/Tools/Sledgehammer/sledgehammer_isar_minimize.ML --- 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 *)) diff -r cddd94fb0e8d -r e0233567a8ef src/HOL/Tools/Sledgehammer/sledgehammer_isar_preplay.ML --- 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 diff -r cddd94fb0e8d -r e0233567a8ef src/HOL/Tools/Sledgehammer/sledgehammer_proof_methods.ML --- 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 | _ =>