1.1 --- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 15:28:11 2013 +0200
     1.2 +++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Thu May 02 16:14:14 2013 +0200
     1.3 @@ -48,7 +48,7 @@
     1.4      * (thm list list * thm list list * Args.src list)
     1.5      * (thm list list * thm list list * Args.src list)
     1.6  
     1.7 -  val datatypes: bool ->
     1.8 +  val co_datatypes: bool ->
     1.9      (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    1.10        binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
    1.11        BNF_FP_Util.fp_result * local_theory) ->
    1.12 @@ -56,7 +56,7 @@
    1.13        ((((binding * binding) * (binding * typ) list) * (binding * term) list) *
    1.14          mixfix) list) list ->
    1.15      local_theory -> local_theory
    1.16 -  val parse_datatype_cmd: bool ->
    1.17 +  val parse_co_datatype_cmd: bool ->
    1.18      (mixfix list -> (string * sort) list option -> binding list -> binding list -> binding list ->
    1.19        binding list list -> typ list * typ list list -> BNF_Def.bnf list -> local_theory ->
    1.20        BNF_FP_Util.fp_result * local_theory) ->
    1.21 @@ -805,7 +805,7 @@
    1.22       (sel_unfold_thmss, sel_corec_thmss, simp_attrs))
    1.23    end;
    1.24  
    1.25 -fun define_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp
    1.26 +fun define_co_datatypes prepare_constraint prepare_typ prepare_term lfp construct_fp
    1.27      (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
    1.28    let
    1.29      (* TODO: sanity checks on arguments *)
    1.30 @@ -1387,14 +1387,15 @@
    1.31            else derive_and_note_coinduct_unfold_corec_thms_for_types);
    1.32  
    1.33      val timer = time (timer ("Constructors, discriminators, selectors, etc., for the new " ^
    1.34 -      (if lfp then "" else "co") ^ "datatype"));
    1.35 +      datatype_word lfp));
    1.36    in
    1.37      timer; lthy'
    1.38    end;
    1.39  
    1.40 -val datatypes = define_datatypes (K I) (K I) (K I);
    1.41 +val co_datatypes = define_co_datatypes (K I) (K I) (K I);
    1.42  
    1.43 -val datatype_cmd = define_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term;
    1.44 +val co_datatype_cmd =
    1.45 +  define_co_datatypes Typedecl.read_constraint Syntax.parse_typ Syntax.parse_term;
    1.46  
    1.47  val parse_ctr_arg =
    1.48    @{keyword "("} |-- parse_binding_colon -- Parse.typ --| @{keyword ")"} ||
    1.49 @@ -1436,8 +1437,8 @@
    1.50    parse_type_args_named_constrained -- parse_binding -- parse_map_rel_bindings --
    1.51    Parse.opt_mixfix -- (@{keyword "="} |-- Parse.enum1 "|" parse_ctr_spec);
    1.52  
    1.53 -val parse_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
    1.54 +val parse_co_datatype = parse_wrap_options -- Parse.and_list1 parse_spec;
    1.55  
    1.56 -fun parse_datatype_cmd lfp construct_fp = parse_datatype >> datatype_cmd lfp construct_fp;
    1.57 +fun parse_co_datatype_cmd lfp construct_fp = parse_co_datatype >> co_datatype_cmd lfp construct_fp;
    1.58  
    1.59  end;

     2.1 --- a/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 15:28:11 2013 +0200
     2.2 +++ b/src/HOL/BNF/Tools/bnf_fp_util.ML	Thu May 02 16:14:14 2013 +0200
     2.3 @@ -120,6 +120,8 @@
     2.4    val mk_dtor_set_inductN: int -> string
     2.5    val mk_set_inductN: int -> string
     2.6  
     2.7 +  val datatype_word: bool -> string
     2.8 +
     2.9    val base_name_of_typ: typ -> string
    2.10    val mk_common_name: string list -> string
    2.11  
    2.12 @@ -320,6 +322,8 @@
    2.13  val sel_unfoldN = selN ^ "_" ^ unfoldN
    2.14  val sel_corecN = selN ^ "_" ^ corecN
    2.15  
    2.16 +fun datatype_word lfp = (if lfp then "" else "co") ^ "datatype";
    2.17 +
    2.18  fun add_components_of_typ (Type (s, Ts)) =
    2.19      fold add_components_of_typ Ts #> cons (Long_Name.base_name s)
    2.20    | add_components_of_typ _ = I;

     3.1 --- a/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 15:28:11 2013 +0200
     3.2 +++ b/src/HOL/BNF/Tools/bnf_gfp.ML	Thu May 02 16:14:14 2013 +0200
     3.3 @@ -3040,6 +3040,6 @@
     3.4  
     3.5  val _ =
     3.6    Outer_Syntax.local_theory @{command_spec "codatatype"} "define BNF-based coinductive datatypes"
     3.7 -    (parse_datatype_cmd false construct_gfp);
     3.8 +    (parse_co_datatype_cmd false construct_gfp);
     3.9  
    3.10  end;

     4.1 --- a/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 15:28:11 2013 +0200
     4.2 +++ b/src/HOL/BNF/Tools/bnf_lfp.ML	Thu May 02 16:14:14 2013 +0200
     4.3 @@ -1862,6 +1862,6 @@
     4.4  
     4.5  val _ =
     4.6    Outer_Syntax.local_theory @{command_spec "datatype_new"} "define BNF-based inductive datatypes"
     4.7 -    (parse_datatype_cmd true construct_lfp);
     4.8 +    (parse_co_datatype_cmd true construct_lfp);
     4.9  
    4.10  end;