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