# HG changeset patch
# User traytel
# Date 1375968625 -7200
# Node ID bdd610910e2c421f5f991caed1181f43584d6f18
# Parent  fe4c2418f06947f3eeabab427b883b6f64d9aea3
tuned

diff -r fe4c2418f069 -r bdd610910e2c src/HOL/BNF/Tools/bnf_gfp.ML
--- 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;
diff -r fe4c2418f069 -r bdd610910e2c src/HOL/BNF/Tools/bnf_gfp_tactics.ML
--- 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 =