# HG changeset patch
# User blanchet
# Date 1327005432 -3600
# Node ID 860b7803c4fa564366d62d07c34490cd01d29656
# Parent  9aad9b87354a3c008ba7c05f4041e89df0c87368
cleanly separate each Metis encoding

diff -r 9aad9b87354a -r 860b7803c4fa src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 19 16:16:13 2012 +0100
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Thu Jan 19 21:37:12 2012 +0100
@@ -399,9 +399,10 @@
   | _ => "Try this"
 
 fun bunch_of_reconstructors needs_full_types lam_trans =
-  [(false, Metis (hd partial_type_encs, lam_trans true)),
-   (true, Metis (full_typesN, lam_trans false)),
+  [(false, Metis (partial_type_enc, lam_trans true)),
+   (true, Metis (full_type_enc, lam_trans false)),
    (false, Metis (no_typesN, lam_trans false)),
+   (true, Metis (really_full_type_enc, lam_trans false)),
    (true, SMT)]
   |> map_filter (fn (full_types, reconstr) =>
                     if needs_full_types andalso not full_types then NONE