--- 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),
--- 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