# HG changeset patch
# User blanchet
# Date 1321613232 -3600
# Node ID da05ce2de5a882288a8e4f12f023cafd0d2cd946
# Parent  9c335d69a36249d0f93812195c93b71609c00d66
better threading of type encodings between Sledgehammer and "metis"

diff -r 9c335d69a362 -r da05ce2de5a8 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
@@ -398,8 +398,8 @@
 
 fun bunch_of_reconstructors needs_full_types lam_trans =
   [(false, Metis (hd partial_type_encs, lam_trans true)),
-   (true, Metis (hd full_type_encs, lam_trans false)),
-   (false, Metis (no_type_enc, lam_trans false)),
+   (true, Metis (full_typesN, lam_trans false)),
+   (false, Metis (no_typesN, lam_trans false)),
    (true, SMT)]
   |> map_filter (fn (full_types, reconstr) =>
                     if needs_full_types andalso not full_types then NONE
@@ -412,7 +412,7 @@
         (if is_none type_enc andalso type_enc' = hd partial_type_encs then
            []
          else
-           [("type_enc", [type_enc'])]) @
+           [("type_enc", [hd (unalias_type_enc type_enc')])]) @
         (if is_none lam_trans andalso lam_trans' = metis_default_lam_trans then
            []
          else