1.1 --- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Nov 18 11:47:12 2011 +0100
     1.2 +++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Nov 18 11:47:12 2011 +0100
     1.3 @@ -45,6 +45,7 @@
     1.4      Proof.context -> (string * locality) list vector -> string proof
     1.5      -> (string * locality) list
     1.6    val is_axiom_used_in_proof : (string list -> bool) -> 'a proof -> bool
     1.7 +  val is_typed_helper : string list -> bool
     1.8    val used_facts_in_unsound_atp_proof :
     1.9      Proof.context -> (string * locality) list vector -> 'a proof
    1.10      -> string list option

     2.1 --- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
     2.3 @@ -145,11 +145,14 @@
     2.4  val reconstructor_names = [metisN, smtN]
     2.5  val plain_metis = Metis (hd partial_type_encs, combinatorsN)
     2.6  
     2.7 -fun standard_reconstructors lam_trans =
     2.8 -  [Metis (hd partial_type_encs, lam_trans),
     2.9 -   Metis (hd full_type_encs, lam_trans),
    2.10 -   Metis (no_type_enc, lam_trans),
    2.11 -   SMT]
    2.12 +fun bunch_of_reconstructors full_types lam_trans =
    2.13 +  if full_types then
    2.14 +    [Metis (hd full_type_encs, lam_trans)]
    2.15 +  else
    2.16 +    [Metis (hd partial_type_encs, lam_trans),
    2.17 +     Metis (hd full_type_encs, lam_trans),
    2.18 +     Metis (no_type_enc, lam_trans),
    2.19 +     SMT]
    2.20  
    2.21  val is_reconstructor = member (op =) reconstructor_names
    2.22  val is_atp = member (op =) o supported_atps
    2.23 @@ -780,8 +783,9 @@
    2.24          NONE =>
    2.25          let
    2.26            val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
    2.27 +          val full_types = is_axiom_used_in_proof is_typed_helper atp_proof
    2.28            val reconstrs =
    2.29 -            standard_reconstructors
    2.30 +            bunch_of_reconstructors full_types
    2.31                  (if member (op =) metis_lam_transs lam_trans then lam_trans
    2.32                   else combinatorsN)
    2.33          in
    2.34 @@ -973,7 +977,7 @@
    2.35          (fn () =>
    2.36              play_one_line_proof mode debug verbose preplay_timeout used_ths
    2.37                                  state subgoal SMT
    2.38 -                                (standard_reconstructors lam_liftingN),
    2.39 +                                (bunch_of_reconstructors false lam_liftingN),
    2.40           fn preplay =>
    2.41              let
    2.42                val one_line_params =