# HG changeset patch
# User blanchet
# Date 1346756551 -7200
# Node ID b815fa776b91f9dfb3a39d79a2f8e5e353d0b773
# Parent  000deee4913ec985a4c88e41439fd0ad41424955
renamed theorem

diff -r 000deee4913e -r b815fa776b91 src/HOL/Codatatype/Tools/bnf_wrap.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:30 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap.ML	Tue Sep 04 13:02:31 2012 +0200
@@ -25,7 +25,7 @@
 val case_congN = "case_cong";
 val case_eqN = "case_eq";
 val casesN = "cases";
-val ctr_selsN = "ctr_sels";
+val collapseN = "collapse";
 val disc_exclusN = "disc_exclus";
 val disc_exhaustN = "disc_exhaust";
 val discsN = "discs";
@@ -350,7 +350,7 @@
                  mk_disc_exhaust_tac n exhaust_thm discI_thms)]
             end;
 
-        val ctr_sel_thms =
+        val collapse_thms =
           let
             fun mk_goal ctr disc sels =
               let
@@ -366,7 +366,7 @@
           in
             map4 (fn m => fn discD => fn sel_thms => Option.map (fn goal =>
               Skip_Proof.prove lthy [] [] goal (fn {context = ctxt, ...} =>
-                mk_ctr_sel_tac ctxt m discD sel_thms))) ms discD_thms sel_thmss goals
+                mk_collapse_tac ctxt m discD sel_thms))) ms discD_thms sel_thmss goals
             |> map_filter I
           end;
 
@@ -437,7 +437,7 @@
           [(case_congN, [case_cong_thm]),
            (case_eqN, [case_eq_thm]),
            (casesN, case_thms),
-           (ctr_selsN, ctr_sel_thms),
+           (collapseN, collapse_thms),
            (discsN, disc_thms),
            (disc_exclusN, disc_exclus_thms),
            (disc_exhaustN, disc_exhaust_thms),
diff -r 000deee4913e -r b815fa776b91 src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
--- a/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Tue Sep 04 13:02:30 2012 +0200
+++ b/src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML	Tue Sep 04 13:02:31 2012 +0200
@@ -9,7 +9,7 @@
 sig
   val mk_case_cong_tac: thm -> thm list -> tactic
   val mk_case_eq_tac: Proof.context -> thm -> thm list -> thm list list -> thm list list -> tactic
-  val mk_ctr_sel_tac: Proof.context -> int -> thm -> thm 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_nchotomy_tac: int -> thm -> tactic
@@ -56,7 +56,7 @@
    EVERY' (map2 (fn k => fn discI =>
      dtac discI THEN' select_prem_tac n (etac @{thm meta_mp}) k THEN' atac) (1 upto n) discIs)) 1;
 
-fun mk_ctr_sel_tac ctxt m discD sel_thms =
+fun mk_collapse_tac ctxt m discD sel_thms =
   (dtac discD THEN'
    (if m = 0 then
       atac