# HG changeset patch # User blanchet # Date 1344950291 -7200 # Node ID 943bb96b4e129ea0cd6a313a66983e127d6ded49 # Parent 5c9356f8c968fa7db95db16307155fed63a29a38 improved set of reconstructor methods diff -r 5c9356f8c968 -r 943bb96b4e12 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 14 14:07:53 2012 +0200 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML Tue Aug 14 15:18:11 2012 +0200 @@ -445,14 +445,18 @@ | _ => "Try this" fun bunch_of_reconstructors needs_full_types lam_trans = - [(false, Metis (partial_type_enc, lam_trans false)), - (true, Metis (full_type_enc, lam_trans false)), - (false, Metis (no_typesN, lam_trans true)), - (true, Metis (really_full_type_enc, lam_trans true)), - (true, SMT)] - |> map_filter (fn (full_types, reconstr) => - if needs_full_types andalso not full_types then NONE - else SOME reconstr) + if needs_full_types then + [Metis (partial_type_enc, lam_trans false), + Metis (full_type_enc, lam_trans false), + Metis (no_typesN, lam_trans true), + Metis (really_full_type_enc, lam_trans true), + SMT] + else + [Metis (full_type_enc, lam_trans false), + Metis (really_full_type_enc, lam_trans false), + Metis (full_type_enc, lam_trans true), + Metis (really_full_type_enc, lam_trans true), + SMT] fun extract_reconstructor ({type_enc, lam_trans, ...} : params) (Metis (type_enc', lam_trans')) = @@ -1058,8 +1062,9 @@ play_one_line_proof mode debug verbose preplay_timeout used_pairs state subgoal SMT (bunch_of_reconstructors false - (fn plain => - if plain then metis_default_lam_trans else liftingN)), + (fn desperate => + if desperate then liftingN + else metis_default_lam_trans)), fn preplay => let val one_line_params =