# HG changeset patch
# User blanchet
# Date 1369722971 -7200
# Node ID 6289b167bbabf41cb130c29dbbb3746252030230
# Parent  014d6b3f5792d74719e5b6ba8886dc4cc4477a16
removed needless comment (yes, sum_case_if is needed)

diff -r 014d6b3f5792 -r 6289b167bbab src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue May 28 08:29:35 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue May 28 08:36:11 2013 +0200
@@ -108,7 +108,6 @@
   unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_comp's @
     map_ids'' @ iter_unfold_thms) THEN rtac refl 1;
 
-(*TODO: sum_case_if needed?*)
 val coiter_unfold_thms =
   @{thms id_def ident_o_ident sum_case_if sum_case_o_inj} @ sum_prod_thms_map;