src/HOL/Codatatype/Tools/bnf_wrap_tactics.ML
changeset 49118 b815fa776b91
parent 49116 3d520eec2746
child 49122 83515378d4d7
--- 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