# HG changeset patch
# User blanchet
# Date 1367504054 -7200
# Node ID d77cf35c27ac522bc6d7a71b96e1cf97199ef8ad
# Parent  b9a8c3b92a62e2af9164cc4af62384d4b180ab7a
tuning names

diff -r b9a8c3b92a62 -r d77cf35c27ac src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 15:28:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 16:14:14 2013 +0200
@@ -48,7 +48,7 @@
     * (thm list list * thm list list * Args.src list)
     * (thm list list * thm list list * Args.src list)
 
-  val datatypes: bool ->
+  val co_datatypes: bool ->
     (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
       binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
       BNF_FP_Util.fp_result * local_theory) ->
@@ -56,7 +56,7 @@
       ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
         mixfix) list) list ->
     local_theory -> local_theory
-  val parse_datatype_cmd: bool ->
+  val parse_co_datatype_cmd: bool ->
     (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
       binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
       BNF_FP_Util.fp_result * local_theory) ->
@@ -805,7 +805,7 @@
      (sel_unfold_thmss, sel_corec_thmss, simp_attrs))
   end;
 
-fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp
+fun define_co_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp
     (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
@@ -1387,14 +1387,15 @@
           else derive_and_note_coinduct_unfold_corec_thms_for_types);
 
     val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
-      (if lfp then "" else "co") ^ "datatype"));
+      datatype_word lfp));
   in
     timer; lthy'
   end;
 
-val datatypes = define_datatypes (K I) (K I) (K I);
+val co_datatypes = define_co_datatypes (K I) (K I) (K I);
 
-val datatype_cmd = define_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term;
+val co_datatype_cmd =
+  define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term;
 
 val parse_ctr_arg =
   @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
@@ -1436,8 +1437,8 @@
   parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
   Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
 
-val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
+val parse_co_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
 
-fun parse_datatype_cmd lfp construct_fp = parse_datatype >> datatype_cmd lfp construct_fp;
+fun parse_co_datatype_cmd lfp construct_fp = parse_co_datatype >> co_datatype_cmd lfp construct_fp;
 
 end;
diff -r b9a8c3b92a62 -r d77cf35c27ac src/HOL/BNF/Tools/bnf_fp_util.ML
--- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 15:28:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 16:14:14 2013 +0200
@@ -120,6 +120,8 @@
   val mk_dtor_set_inductN: int -> string
   val mk_set_inductN: int -> string
 
+  val datatype_word: bool -> string
+
   val base_name_of_typ: typ -> string
   val mk_common_name: string list -> string
 
@@ -320,6 +322,8 @@
 val sel_unfoldN = selN ^ "_" ^ unfoldN
 val sel_corecN = selN ^ "_" ^ corecN
 
+fun datatype_word lfp = (if lfp then "" else "co") ^ "datatype";
+
 fun add_components_of_typ (Type (s, Ts)) =
     fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
   | add_components_of_typ _ = I;
diff -r b9a8c3b92a62 -r d77cf35c27ac src/HOL/BNF/Tools/bnf_gfp.ML
--- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 15:28:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 16:14:14 2013 +0200
@@ -3040,6 +3040,6 @@
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
-    (parse_datatype_cmd false construct_gfp);
+    (parse_co_datatype_cmd false construct_gfp);
 
 end;
diff -r b9a8c3b92a62 -r d77cf35c27ac src/HOL/BNF/Tools/bnf_lfp.ML
--- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 15:28:11 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 16:14:14 2013 +0200
@@ -1862,6 +1862,6 @@
 
 val _ =
   Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes"
-    (parse_datatype_cmd true construct_lfp);
+    (parse_co_datatype_cmd true construct_lfp);
 
 end;