src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML
changeset 55083 0a689157e3ce
parent 55061 a0adf838e2d1
child 55414 eab03e9cee8a
     1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jan 20 20:00:33 2014 +0100
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jan 20 20:21:12 2014 +0100
     1.3 @@ -41,7 +41,7 @@
     1.4        Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
     1.5        mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
     1.6  val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0;
     1.7 -val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps id_apply};
     1.8 +val sum_prod_thms_rel = @{thms prod_rel_apply sum_rel_simps id_apply};
     1.9  
    1.10  fun hhf_concl_conv cv ctxt ct =
    1.11    (case Thm.term_of ct of