# HG changeset patch
# User blanchet
# Date 1375889020 -7200
# Node ID 3ff23987f316d07ca90e20990ea00de6f06f8a79
# Parent  2af1caada147abe3e4ec3f6d30e12048368e1f44
tuning

diff -r 2af1caada147 -r 3ff23987f316 src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- 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;
diff -r 2af1caada147 -r 3ff23987f316 src/HOL/BNF/Tools/bnf_fp_util.ML
--- 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)