# HG changeset patch
# User blanchet
# Date 1321613232 -3600
# Node ID 211a6e6cbc04becc97a638833fcee5b9eb5d91af
# Parent  8e3891309a8eba6f3f4ff438bad02fa54c4b993f
move eta-contraction to before translation to Metis, to ensure everything stays in sync

diff -r 8e3891309a8e -r 211a6e6cbc04 src/HOL/Tools/ATP/atp_translate.ML
--- a/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/ATP/atp_translate.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -692,7 +692,7 @@
   | open_form t = t
 
 fun lift_lams_part_1 ctxt type_enc =
-  map (Envir.eta_contract #> close_form) #> rpair ctxt
+  map close_form #> rpair ctxt
   #-> Lambda_Lifting.lift_lambdas
           (SOME ((if polymorphism_of_type_enc type_enc = Polymorphic then
                     lam_lifted_poly_prefix
diff -r 8e3891309a8e -r 211a6e6cbc04 src/HOL/Tools/Metis/metis_tactic.ML
--- a/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 11:47:12 2011 +0100
+++ b/src/HOL/Tools/Metis/metis_tactic.ML	Fri Nov 18 11:47:12 2011 +0100
@@ -72,7 +72,6 @@
     th
   else
     let
-      val th = th |> Drule.eta_contraction_rule
       fun conv wrap ctxt ct =
         if Meson_Clausify.is_quasi_lambda_free (term_of ct) then
           Thm.reflexive ct
@@ -105,6 +104,8 @@
   let val thy = Proof_Context.theory_of ctxt
       val new_skolemizer =
         Config.get ctxt new_skolemizer orelse null (Meson.choice_theorems thy)
+      val cls = cls |> map Drule.eta_contraction_rule
+      val ths0 = ths0 |> map Drule.eta_contraction_rule
       val th_cls_pairs =
         map2 (fn j => fn th =>
                 (Thm.get_name_hint th,