1.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Sun Jul 27 21:20:11 2014 +0200
     1.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar.ML	Mon Jul 28 12:31:30 2014 +0200
     1.3 @@ -1467,7 +1467,8 @@
     1.4                        val thm = Goal.prove_sorry lthy [] [] goal
     1.5                            (fn {context = ctxt, prems = _} =>
     1.6                              mk_rel_cases_tac ctxt (certify ctxt ta) (certify ctxt tb) exhaust
     1.7 -                              injects rel_inject_thms distincts rel_distinct_thms)
     1.8 +                              injects rel_inject_thms distincts rel_distinct_thms
     1.9 +                              (map rel_eq_of_bnf live_nesting_bnfs))
    1.10                          |> singleton (Proof_Context.export names_lthy lthy)
    1.11                          |> Thm.close_derivation;
    1.12  

     2.1 --- a/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Sun Jul 27 21:20:11 2014 +0200
     2.2 +++ b/src/HOL/Tools/BNF/bnf_fp_def_sugar_tactics.ML	Mon Jul 28 12:31:30 2014 +0200
     2.3 @@ -28,7 +28,7 @@
     2.4    val mk_rec_tac: thm list -> thm list -> thm list -> thm -> thm -> thm -> thm -> Proof.context ->
     2.5      tactic
     2.6    val mk_rel_cases_tac:  Proof.context -> cterm -> cterm -> thm -> thm list -> thm list ->
     2.7 -    thm list -> thm list -> tactic
     2.8 +    thm list -> thm list -> thm list -> tactic
     2.9    val mk_rel_coinduct0_tac: Proof.context -> thm -> cterm list -> thm list -> thm list ->
    2.10      thm list list -> thm list list -> thm list list -> thm list -> thm list -> thm list ->
    2.11      thm list -> thm list -> thm list -> tactic
    2.12 @@ -216,11 +216,11 @@
    2.13        (1 upto nn) ns pre_rel_defs fp_abs_inverses abs_inverses dtor_ctors exhausts ctr_defss discsss
    2.14        selsss));
    2.15  
    2.16 -fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts =
    2.17 +fun mk_rel_cases_tac ctxt ct1 ct2 exhaust injects rel_injects distincts rel_distincts rel_eqs=
    2.18    HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
    2.19      rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
    2.20        hyp_subst_tac ctxt) THEN
    2.21 -  unfold_thms_tac ctxt (injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
    2.22 +  unfold_thms_tac ctxt (rel_eqs @ injects @ rel_injects @ @{thms conj_imp_eq_imp_imp simp_thms(6)
    2.23      True_implies_equals conj_imp_eq_imp_imp} @
    2.24      map (fn thm => thm RS eqFalseI) (distincts @ rel_distincts) @
    2.25      map (fn thm => thm RS eqTrueI) rel_injects) THEN
    2.26 @@ -260,7 +260,7 @@
    2.27          unfold_tac ctxt (ctor_inject :: rel_pre_list_def :: ctor_defs @ nesting_rel_eqs @
    2.28            @{thms BNF_Comp.id_bnf_comp_def vimage2p_def}) THEN
    2.29          TRYALL (hyp_subst_tac ctxt) THEN
    2.30 -        unfold_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
    2.31 +        unfold_thms_tac ctxt (Abs_inverse :: @{thms rel_sum_simps rel_prod_apply Inl_Inr_False
    2.32            Inr_Inl_False  sum.inject prod.inject}) THEN
    2.33          TRYALL (etac FalseE ORELSE' (REPEAT_DETERM o etac conjE) THEN' atac))
    2.34      cterms exhausts ctor_defss ctor_injects rel_pre_list_defs Abs_inverses);
    2.35 @@ -269,7 +269,7 @@
    2.36    HEADGOAL (rtac (cterm_instantiate_pos [SOME ct1] exhaust) THEN_ALL_NEW
    2.37      rtac (cterm_instantiate_pos [SOME ct2] exhaust) THEN_ALL_NEW
    2.38        hyp_subst_tac ctxt) THEN
    2.39 -  Local_Defs.unfold_tac ctxt (sels @ rel_injects @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
    2.40 +  unfold_thms_tac ctxt (sels @ rel_injects @ @{thms simp_thms(6,7,8,11,12,15,16,21,22,24)} @
    2.41      ((discs @ distincts) RL @{thms iffD2[OF eq_True] iffD2[OF eq_False]}) @
    2.42      (rel_injects RL @{thms iffD2[OF eq_True]}) @
    2.43      (rel_distincts RL @{thms iffD2[OF eq_False]})) THEN