src/HOL/Codatatype/Tools/bnf_wrap.ML

 
 structure BNF_Wrap : BNF_WRAP =
 struct
 
 open BNF_Util
-open BNF_FP_Util
 open BNF_Wrap_Tactics
 
 val is_N = "is_";
 val un_N = "un_";
 fun mk_un_N 1 1 suf = un_N ^ suf

 val ctr_selsN = "ctr_sels";
 val disc_exclusN = "disc_exclus";
 val disc_exhaustN = "disc_exhaust";
 val discsN = "discs";
 val distinctN = "distinct";
+val exhaustN = "exhaust";
+val injectN = "inject";
+val nchotomyN = "nchotomy";
 val selsN = "sels";
 val splitN = "split";
 val split_asmN = "split_asm";
 val weak_case_cong_thmsN = "weak_case_cong";