# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1271768153 -7200
# Node ID ff2580df7cccc3280700b20478f9b4ac65a13431
# Parent  4df49260bd82a92e2505d0ace9f323637520d488
eta-normalize the goal since the original theorem is atomized

diff -r 4df49260bd82 -r ff2580df7ccc src/HOL/Tools/Quotient/quotient_tacs.ML
--- a/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Apr 20 11:31:14 2010 +0200
+++ b/src/HOL/Tools/Quotient/quotient_tacs.ML	Tue Apr 20 14:55:53 2010 +0200
@@ -653,10 +653,13 @@
 
 fun lifted qtys ctxt thm =
 let
-  val ((_, [thm']), ctxt') = Variable.import false [thm] ctxt
-  val goal = (quotient_lift_all qtys ctxt' o prop_of) thm'
+  (* When the theorem is atomized, eta redexes are contracted,
+     so we do it both in the original theorem *)
+  val thm' = Drule.eta_contraction_rule thm
+  val ((_, [thm'']), ctxt') = Variable.import false [thm'] ctxt
+  val goal = (quotient_lift_all qtys ctxt' o prop_of) thm''
 in
-  Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm] 1))
+  Goal.prove ctxt' [] [] goal (K (lift_tac ctxt' [thm'] 1))
   |> singleton (ProofContext.export ctxt' ctxt)
 end;