# HG changeset patch
# User traytel
# Date 1367932846 -7200
# Node ID e0bf21531ed52b30bcc63da666e363686b7a5144
# Parent  7c43b8df0f5d1b72234e56596e88ea0493275a62
do not unfold the definition of the relator as it is not defined in terms of srel anymore

diff -r 7c43b8df0f5d -r e0bf21531ed5 src/HOL/BNF/Tools/bnf_comp.ML
--- 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);