# HG changeset patch
# User blanchet
# Date 1369722972 -7200
# Node ID 056ec8201667933b7d6aa598051ee90f31c45c20
# Parent  6289b167bbabf41cb130c29dbbb3746252030230
clean up list of theorems

diff -r 6289b167bbab -r 056ec8201667 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 28 08:36:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Tue May 28 08:36:12 2013 +0200
@@ -1018,9 +1018,8 @@
       ||>> mk_TFrees nn
       ||>> variant_tfrees fp_b_names;
 
-    (* TODO: cleaner handling of fake contexts, without "background_theory" *)
-    (*the "perhaps o try" below helps gracefully handles the case where the new type is defined in a
-      locale and shadows an existing global type*)
+    (* TODO: Cleaner handling of fake contexts, without "background_theory". The case where the new
+       type is defined in a locale and shadows an existing global type is currently not handled. *)
 
     fun add_fake_type spec =
       Sign.add_type no_defs_lthy (type_binding_of spec,
diff -r 6289b167bbab -r 056ec8201667 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:36:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar_tactics.ML	Tue May 28 08:36:12 2013 +0200
@@ -99,10 +99,9 @@
   unfold_thms_tac ctxt [ctr_def] THEN rtac (ctor_inject RS ssubst) 1 THEN
   unfold_thms_tac ctxt @{thms sum.inject Pair_eq conj_assoc} THEN rtac refl 1;
 
-(*TODO: Try "sum_prod_thms_map" here, enriched with a few theorems*)
 val iter_unfold_thms =
-  @{thms comp_def convol_def fst_conv id_def map_pair_simp prod_case_Pair_iden snd_conv split_conv
-      sum.simps(5,6) sum_map.simps unit_case_Unity};
+  @{thms comp_def convol_def fst_conv id_def prod_case_Pair_iden snd_conv
+      split_conv unit_case_Unity} @ sum_prod_thms_map;
 
 fun mk_iter_tac pre_map_defs map_comp's map_ids'' iter_defs ctor_iter ctr_def ctxt =
   unfold_thms_tac ctxt (ctr_def :: ctor_iter :: iter_defs @ pre_map_defs @ map_comp's @