1.1 --- a/src/HOL/Codatatype/Examples/Misc_Data.thy	Tue Sep 18 11:06:25 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Examples/Misc_Data.thy	Tue Sep 18 11:41:04 2012 +0200
     1.3 @@ -145,8 +145,8 @@
     1.4   and s8 = S8 nat
     1.5  *)
     1.6  
     1.7 -data ('a, 'b) bar = BAR "'b \<Rightarrow> 'a"
     1.8 -data ('a, 'b, 'c, 'd) foo = FOO "'d + 'b \<Rightarrow> 'c + 'a"
     1.9 +data ('a, 'b) bar = Bar "'b \<Rightarrow> 'a"
    1.10 +data ('a, 'b, 'c, 'd) foo = Foo "'d + 'b \<Rightarrow> 'c + 'a"
    1.11  
    1.12  data 'a dead_foo = A
    1.13  data ('a, 'b) use_dead_foo = Y "'a" "'b dead_foo"

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 18 11:06:25 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 18 11:41:04 2012 +0200
     2.3 @@ -87,18 +87,15 @@
     2.4    Local_Defs.unfold_tac ctxt @{thms id_def} THEN
     2.5    TRY ((rtac refl ORELSE' subst_tac ctxt @{thms unit_eq} THEN' rtac refl) 1);
     2.6  
     2.7 -val maybe_singletonI_tac = atac ORELSE' rtac @{thm singletonI};
     2.8 -
     2.9  val solve_prem_prem_tac =
    2.10    REPEAT o (eresolve_tac @{thms bexE rev_bexI} ORELSE' rtac @{thm rev_bexI[OF UNIV_I]} ORELSE'
    2.11      hyp_subst_tac ORELSE' resolve_tac @{thms disjI1 disjI2}) THEN'
    2.12    (rtac refl ORELSE' atac ORELSE' rtac @{thm singletonI});
    2.13  
    2.14  val induct_prem_prem_thms =
    2.15 -  @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_assoc Un_empty_left Un_empty_right Un_iff
    2.16 -      Union_Un_distrib collect_def[abs_def] fst_conv image_def o_apply snd_conv snd_prod_fun
    2.17 -      sum.cases sup_bot_right fst_map_pair map_pair_simp mem_Collect_eq mem_UN_compreh_eq
    2.18 -      prod_set_simps sum_map.simps sum_set_simps};
    2.19 +  @{thms SUP_empty Sup_empty Sup_insert UN_insert Un_empty_left Un_empty_right Un_iff
    2.20 +      Union_Un_distrib collect_def[abs_def] image_def o_apply map_pair_simp
    2.21 +      mem_Collect_eq mem_UN_compreh_eq prod_set_simps sum_map.simps sum_set_simps};
    2.22  
    2.23  fun mk_induct_leverage_prem_prems_tac ctxt nn kks set_natural's pre_set_defs =
    2.24    EVERY' (maps (fn kk => [select_prem_tac nn (dtac meta_spec) kk, etac meta_mp,