# HG changeset patch
# User blanchet
# Date 1346756707 -7200
# Node ID 83515378d4d752cbeba084e2536ca704f6e5f464
# Parent  9e0acaa470abb2f66262e1255fd20ffc6b44e712
renamed "disc_exclus" theorem to "disc_exclude"

diff -r 9e0acaa470ab -r 83515378d4d7 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:05:01 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:05:07 2012 +0200
@@ -28,7 +28,7 @@
 val case_eqN = "case_eq";
 val casesN = "cases";
 val collapseN = "collapse";
-val disc_exclusN = "disc_exclus";
+val disc_excludeN = "disc_exclude";
 val disc_exhaustN = "disc_exhaust";
 val discsN = "discs";
 val distinctN = "distinct";
@@ -334,7 +334,7 @@
 
         val disc_thms = flat (map2 (fn true => K [] | false => I) no_discs disc_thmss);
 
-        val disc_exclus_thms =
+        val disc_exclude_thms =
           if has_not_other_disc_def then
             []
           else
@@ -352,12 +352,12 @@
               val goal_halvess = map mk_goal half_pairss;
               val half_thmss =
                 map3 (fn [] => K (K []) | [goal] => fn [((((m, discD), _), _), _)] => fn disc_thm =>
-                  [prove (mk_half_disc_exclus_tac m discD disc_thm) goal])
+                  [prove (mk_half_disc_exclude_tac m discD disc_thm) goal])
                 goal_halvess half_pairss (flat disc_thmss');
 
               val goal_other_halvess = map (mk_goal o map swap) half_pairss;
               val other_half_thmss =
-                map2 (map2 (prove o mk_other_half_disc_exclus_tac)) half_thmss goal_other_halvess;
+                map2 (map2 (prove o mk_other_half_disc_exclude_tac)) half_thmss goal_other_halvess;
             in
               interleave (flat half_thmss) (flat other_half_thmss)
             end;
@@ -463,7 +463,7 @@
            (casesN, case_thms),
            (collapseN, collapse_thms),
            (discsN, disc_thms),
-           (disc_exclusN, disc_exclus_thms),
+           (disc_excludeN, disc_exclude_thms),
            (disc_exhaustN, disc_exhaust_thms),
            (distinctN, distinct_thms),
            (exhaustN, [exhaust_thm]),
diff -r 9e0acaa470ab -r 83515378d4d7 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Tue Sep 04 13:05:01 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Tue Sep 04 13:05:07 2012 +0200
@@ -11,10 +11,10 @@
   val mk_case_eq_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
   val mk_collapse_tac: Proof.context -> int -> thm -> thm list -> tactic
   val mk_disc_exhaust_tac: int -> thm -> thm list -> tactic
-  val mk_half_disc_exclus_tac: int -> thm -> thm -> tactic
+  val mk_half_disc_exclude_tac: int -> thm -> thm -> tactic
   val mk_nchotomy_tac: int -> thm -> tactic
   val mk_not_other_disc_def_tac: Proof.context -> thm -> thm -> thm -> tactic
-  val mk_other_half_disc_exclus_tac: thm -> tactic
+  val mk_other_half_disc_exclude_tac: thm -> tactic
   val mk_split_tac: thm -> thm list -> thm list list -> thm list list list -> tactic
   val mk_split_asm_tac: Proof.context -> thm -> tactic
 end;
@@ -42,13 +42,13 @@
     SELECT_GOAL (Local_Defs.unfold_tac ctxt [not_ex]), REPEAT_DETERM o rtac allI, rtac distinct,
     rtac exhaust', etac notE, atac, REPEAT_DETERM o rtac exI, atac] 1;
 
-fun mk_half_disc_exclus_tac m discD disc'_thm =
+fun mk_half_disc_exclude_tac m discD disc'_thm =
   (dtac discD THEN'
    REPEAT_DETERM_N m o etac exE THEN'
    hyp_subst_tac THEN'
    rtac disc'_thm) 1;
 
-fun mk_other_half_disc_exclus_tac half_thm =
+fun mk_other_half_disc_exclude_tac half_thm =
   (etac @{thm contrapos_pn} THEN' etac half_thm) 1;
 
 fun mk_disc_exhaust_tac n exhaust discIs =