--- a/src/HOL/BNF/Tools/bnf_comp.ML Mon Jul 15 14:23:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_comp.ML Mon Jul 15 15:50:39 2013 +0200
@@ -331,8 +331,7 @@
rel_conversep_of_bnf bnf RS sym], rel_Grp],
trans OF [rel_OO_of_bnf bnf RS sym, rel_cong_of_bnf bnf OF
(replicate n @{thm trans[OF Grp_UNIV_id[OF refl] eq_alt[symmetric]]} @
- replicate (live - n) @{thm Grp_fst_snd})]]] RS sym)
- (*|> unfold_thms lthy (rel_def_of_bnf bnf :: @{thms Id_def' mem_Collect_eq split_conv})*);
+ replicate (live - n) @{thm Grp_fst_snd})]]] RS sym);
in
rtac thm 1
end;