do not unfold the definition of the relator as it is not defined in terms of srel anymore

--- a/src/HOL/BNF/Tools/bnf_comp.ML	Tue May 07 14:47:22 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML	Tue May 07 15:20:46 2013 +0200
@@ -648,7 +648,7 @@
       (mk_tac (map_cong0_of_bnf bnf)) (map mk_tac (set_map_of_bnf bnf))
       (K (rtac bd_card_order 1)) (K (rtac bd_cinfinite 1)) (map mk_tac set_bds) (mk_tac in_bd)
       (mk_tac (map_wpull_of_bnf bnf))
-      (mk_tac (unfold_thms lthy [rel_def_of_bnf bnf] (rel_OO_Grp_of_bnf bnf)));
+      (mk_tac (rel_OO_Grp_of_bnf bnf));
 
     val bnf_wits = map snd (mk_wits_of_bnf (replicate nwits Ds) (replicate nwits As) bnf);