1.1 --- a/src/HOL/Codatatype/BNF_Library.thy	Mon Sep 10 17:36:02 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/BNF_Library.thy	Mon Sep 10 17:52:01 2012 +0200
     1.3 @@ -829,6 +829,9 @@
     1.4  lemma one_pointE: "\<lbrakk>\<And>x. s = x \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P"
     1.5  by simp
     1.6  
     1.7 +lemma obj_one_pointE: "\<forall>x. s = x \<longrightarrow> P \<Longrightarrow> P"
     1.8 +by blast
     1.9 +
    1.10  lemma obj_sumE_f:
    1.11  "\<lbrakk>\<forall>x. s = f (Inl x) \<longrightarrow> P; \<forall>x. s = f (Inr x) \<longrightarrow> P\<rbrakk> \<Longrightarrow> \<forall>x. s = f x \<longrightarrow> P"
    1.12  by (metis sum.exhaust)

     2.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:36:02 2012 +0200
     2.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar.ML	Mon Sep 10 17:52:01 2012 +0200
     2.3 @@ -72,15 +72,8 @@
     2.4  fun mk_sumEN_balanced 1 = @{thm one_pointE}
     2.5    | mk_sumEN_balanced 2 = @{thm sumE} (*optimization*)
     2.6    | mk_sumEN_balanced n =
     2.7 -    let
     2.8 -      val thm =
     2.9 -        Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
    2.10 -          (replicate n asm_rl) OF (replicate n (impI RS allI));
    2.11 -      val f as (_, f_T) =
    2.12 -        Term.add_vars (prop_of thm) []
    2.13 -        |> filter (fn ((s, _), _) => s = "f") |> the_single;
    2.14 -      val inst = [pairself (cterm_of @{theory}) (Var f, Abs (Name.uu, domain_type f_T, Bound 0))];
    2.15 -    in cterm_instantiate inst thm end;
    2.16 +    Balanced_Tree.make (fn (thm1, thm2) => thm1 RSN (1, thm2 RSN (2, @{thm obj_sumE_f})))
    2.17 +      (replicate n asm_rl) OF (replicate n (impI RS allI)) RS @{thm obj_one_pointE};
    2.18  
    2.19  fun tick v f = Term.lambda v (HOLogic.mk_prod (v, f $ v));
    2.20  

     3.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 10 17:36:02 2012 +0200
     3.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Mon Sep 10 17:52:01 2012 +0200
     3.3 @@ -30,11 +30,7 @@
     3.4     rtac refl) 1;
     3.5  
     3.6  fun mk_exhaust_tac ctxt n ctr_defs fld_iff_unf sumEN' =
     3.7 -print_tac "A1" THEN(*###*)
     3.8 -  Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN
     3.9 -print_tac ("A2: " ^ Display.string_of_thm ctxt sumEN') THEN(*###*)
    3.10 -  rtac sumEN' 1 THEN
    3.11 -print_tac "A3" THEN(*###*)
    3.12 +  Local_Defs.unfold_tac ctxt (fld_iff_unf :: ctr_defs) THEN rtac sumEN' 1 THEN
    3.13    Local_Defs.unfold_tac ctxt @{thms all_prod_eq} THEN
    3.14    EVERY' (maps (fn k => [select_prem_tac n (rotate_tac 1) k, REPEAT_DETERM o dtac @{thm meta_spec},
    3.15      etac @{thm meta_mp}, atac]) (1 upto n)) 1;