eta-normalize the goal since the original theorem is atomized

--- 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;