src/HOL/BNF/Tools/bnf_def.ML

--- a/src/HOL/BNF/Tools/bnf_def.ML	Fri Sep 28 08:59:54 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_def.ML	Fri Sep 28 09:12:49 2012 +0200
@@ -1125,7 +1125,8 @@
 
         fun mk_rel_eq () =
           unfold_thms lthy (bnf_srel_def :: mem_Collect_etc')
-            (Lazy.force srel_Id RS @{thm arg_cong[of _ _ "%A x y. (x, y) : A"]});
+            (Lazy.force srel_Id RS @{thm arg_cong[of _ _ "%A x y. (x, y) : A"]})
+          |> Drule.eta_contraction_rule;
 
         val rel_eq = Lazy.lazy mk_rel_eq;