# HG changeset patch
# User blanchet
# Date 1347961264 -7200
# Node ID 37cae324d73ef46879cd69104a78197ec8144c18
# Parent  483007ddbdc2a996d2da02e3082844436087f569
further tuned simpset

diff -r 483007ddbdc2 -r 37cae324d73e src/HOL/Codatatype/Examples/Misc_Data.thy
--- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Tue Sep 18 11:06:25 2012 +0200
+++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Tue Sep 18 11:41:04 2012 +0200
@@ -145,8 +145,8 @@
  and s8 = S8 nat
 *)
 
-data ('a, 'b) bar = BAR "'b \<Rightarrow> 'a"
-data ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
+data ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
+data ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
 
 data 'a dead_foo = A
 data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"
diff -r 483007ddbdc2 -r 37cae324d73e src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 18 11:06:25 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 18 11:41:04 2012 +0200
@@ -87,18 +87,15 @@
   Local_Defs.unfold_tac ctxt @{thms id_def} THEN
   TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
 
-val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};
-
 val solve_prem_prem_tac =
   REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
     hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
   (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
 
 val induct_prem_prem_thms =
-  @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_assoc Un_empty_left Un_empty_right Un_iff
-      Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv snd_prod_fun
-      sum.cases sup_bot_right fst_map_pair map_pair_simp mem_Collect_eq mem_UN_compreh_eq
-      prod_set_simps sum_map.simps sum_set_simps};
+  @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
+      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};
 
 fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
   EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,