--- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 12:17:26 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML Thu Mar 06 13:36:15 2014 +0100
@@ -37,11 +37,11 @@
val basic_simp_thms = @{thms simp_thms(7,8,12,14,22,24)};
val more_simp_thms = basic_simp_thms @ @{thms simp_thms(11,15,16,21)};
-val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case sum_map.simps};
+val sum_prod_thms_map = @{thms id_apply map_pair_simp prod.case sum.case map_sum.simps};
val sum_prod_thms_set =
@{thms UN_empty UN_insert Un_empty_left Un_empty_right Un_iff UN_simps(10) UN_iff
Union_Un_distrib image_iff o_apply map_pair_simp
- mem_Collect_eq prod_set_simps sum_map.simps sum_set_simps};
+ mem_Collect_eq prod_set_simps map_sum.simps sum_set_simps};
val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply};
fun hhf_concl_conv cv ctxt ct =