# HG changeset patch
# User blanchet
# Date 1348838612 -7200
# Node ID 71294d8c36fb11e8a90df7940d60fc693ef2b9e8
# Parent  9f884142334cba0fbfd6a9011ec730a07a67319a
simplified simpset

diff -r 9f884142334c -r 71294d8c36fb src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Sep 28 15:14:11 2012 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Fri Sep 28 15:23:32 2012 +0200
@@ -42,10 +42,7 @@
       Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
       mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
 val sum_prod_thms_set = @{thms UN_compreh_eq_eq} @ sum_prod_thms_set0;
-(* FIXME: Need "prod.cases" and "sum.cases"? And why "sum.inject" but no "prod.inject"? *)
-val sum_prod_thms_rel =
-  @{thms prod.cases prod_rel_simp sum.cases sum_rel_simps
-      sum.inject sum.distinct[THEN eq_False[THEN iffD2]]};
+val sum_prod_thms_rel = @{thms prod_rel_simp sum_rel_simps};
 
 val ss_if_True_False = ss_only @{thms if_True if_False};