--- a/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 14:48:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML Thu Aug 08 15:30:25 2013 +0200
@@ -210,7 +210,7 @@
val bd_Cinfinite = hd bd_Cinfinites;
val in_monos = map in_mono_of_bnf bnfs;
val map_comps = map map_comp_of_bnf bnfs;
- val sym_map_comps = map (fn thm => thm RS sym) map_comps;
+ val sym_map_comps = map mk_sym map_comps;
val map_comp's = map map_comp'_of_bnf bnfs;
val map_cong0s = map map_cong0_of_bnf bnfs;
val map_ids = map map_id_of_bnf bnfs;
--- a/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 08 14:48:19 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp_tactics.ML Thu Aug 08 15:30:25 2013 +0200
@@ -1061,7 +1061,7 @@
EVERY' (map (fn thm => rtac @{thm UN_least} THEN' etac thm) set_hset_incl_hsets)] 1;
fun mk_map_id_tac maps unfold_unique unfold_dtor =
- EVERY' [rtac (unfold_unique RS trans), EVERY' (map (fn thm => rtac (thm RS sym)) maps),
+ EVERY' [rtac (unfold_unique RS trans), EVERY' (map (rtac o mk_sym) maps),
rtac unfold_dtor] 1;
fun mk_map_comp_tac m n maps map_comps map_cong0s unfold_unique =