# HG changeset patch
# User blanchet
# Date 1344950805 -7200
# Node ID b86e8cf3f4648a24cf744812198ffc287c64bc8d
# Parent  55874425fd32701583fd29618ac3f0f893b55074
fixed then-else confusion

diff -r 55874425fd32 -r b86e8cf3f464 src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 14 15:23:28 2012 +0200
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML	Tue Aug 14 15:26:45 2012 +0200
@@ -446,17 +446,17 @@
 
 fun bunch_of_reconstructors needs_full_types lam_trans =
   if needs_full_types then
+    [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]
+  else
     [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')) =