--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Aug 07 17:23:40 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML Wed Aug 07 17:23:40 2013 +0200
@@ -1433,7 +1433,7 @@
else derive_and_note_coinduct_coiters_thms_for_types);
val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
- datatype_word fp));
+ co_prefix fp ^ "datatype"));
in
timer; lthy''
end;
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Aug 07 17:23:40 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML Wed Aug 07 17:23:40 2013 +0200
@@ -124,7 +124,7 @@
val mk_dtor_set_inductN: int -> string
val mk_set_inductN: int -> string
- val datatype_word: fp_kind -> string
+ val co_prefix: fp_kind -> string
val base_name_of_typ: typ -> string
val mk_common_name: string list -> string
@@ -338,7 +338,7 @@
val sel_unfoldN = selN ^ "_" ^ unfoldN
val sel_corecN = selN ^ "_" ^ corecN
-fun datatype_word fp = (if fp = Greatest_FP then "co" else "") ^ "datatype";
+fun co_prefix fp = (if fp = Greatest_FP then "co" else "");
fun add_components_of_typ (Type (s, Ts)) =
fold add_components_of_typ Ts #> cons (Long_Name.base_name s)