1.1 --- a/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 16:17:22 2012 +0200
     1.2 +++ b/src/HOL/Codatatype/Tools/bnf_fp_sugar_tactics.ML	Tue Sep 04 16:27:27 2012 +0200
     1.3 @@ -10,6 +10,7 @@
     1.4    val mk_exhaust_tac: Proof.context -> int -> int list -> thm list -> thm -> thm -> tactic
     1.5    val mk_fld_iff_unf_tac: Proof.context -> ctyp option list -> cterm -> cterm -> thm -> thm
     1.6      -> tactic
     1.7 +  val mk_half_distinct_tac: Proof.context -> thm -> thm list -> tactic
     1.8    val mk_inject_tac: Proof.context -> thm -> thm -> tactic
     1.9  end;
    1.10  
    1.11 @@ -34,6 +35,10 @@
    1.12       SELECT_GOAL (Local_Defs.unfold_tac ctxt [th]) THEN'
    1.13       atac) [rev cTs, cTs] [cunf, cfld] [unf_fld, fld_unf])) 1;
    1.14  
    1.15 +fun mk_half_distinct_tac ctxt fld_inject ctr_defs =
    1.16 +  Local_Defs.unfold_tac ctxt (fld_inject :: @{thms sum.inject} @ ctr_defs) THEN
    1.17 +  rtac @{thm sum.distinct(1)} 1;
    1.18 +
    1.19  fun mk_inject_tac ctxt ctr_def fld_inject =
    1.20    Local_Defs.unfold_tac ctxt [ctr_def] THEN
    1.21    rtac (fld_inject RS ssubst) 1 THEN