# HG changeset patch
# User blanchet
# Date 1321613232 -3600
# Node ID 8d1545420a05e44160dcc334e4fb435aabeb72bc
# Parent  d2139b4557fc3a7787ed3e065c255c6d51d3ad3d
no needless reconstructors

diff -r d2139b4557fc -r 8d1545420a05 src/HOL/Tools/ATP/atp_reconstruct.ML
--- a/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_reconstruct.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -45,6 +45,7 @@
     Proof.context -> (string * locality) list vector -> string proof
     -> (string * locality) list
   val is_axiom_used_in_proof : (string list -> bool) -> 'a proof -> bool
+  val is_typed_helper : string list -> bool
   val used_facts_in_unsound_atp_proof :
     Proof.context -> (string * locality) list vector -> 'a proof
     -> string list option
diff -r d2139b4557fc -r 8d1545420a05 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -145,11 +145,14 @@
 val reconstructor_names = [metisN, smtN]
 val plain_metis = Metis (hd partial_type_encs, combinatorsN)
 
-fun standard_reconstructors lam_trans =
-  [Metis (hd partial_type_encs, lam_trans),
-   Metis (hd full_type_encs, lam_trans),
-   Metis (no_type_enc, lam_trans),
-   SMT]
+fun bunch_of_reconstructors full_types lam_trans =
+  if full_types then
+    [Metis (hd full_type_encs, lam_trans)]
+  else
+    [Metis (hd partial_type_encs, lam_trans),
+     Metis (hd full_type_encs, lam_trans),
+     Metis (no_type_enc, lam_trans),
+     SMT]
 
 val is_reconstructor = member (op =) reconstructor_names
 val is_atp = member (op =) o supported_atps
@@ -780,8 +783,9 @@
         NONE =>
         let
           val used_facts = used_facts_in_atp_proof ctxt fact_names atp_proof
+          val full_types = is_axiom_used_in_proof is_typed_helper atp_proof
           val reconstrs =
-            standard_reconstructors
+            bunch_of_reconstructors full_types
                 (if member (op =) metis_lam_transs lam_trans then lam_trans
                  else combinatorsN)
         in
@@ -973,7 +977,7 @@
         (fn () =>
             play_one_line_proof mode debug verbose preplay_timeout used_ths
                                 state subgoal SMT
-                                (standard_reconstructors lam_liftingN),
+                                (bunch_of_reconstructors false lam_liftingN),
          fn preplay =>
             let
               val one_line_params =