--- a/NEWS Fri Aug 30 12:09:51 2013 +0200
+++ b/NEWS Fri Aug 30 12:12:41 2013 +0200
@@ -158,7 +158,7 @@
* HOL/BNF:
- Various improvements to BNF-based (co)datatype package, including a
- "primrec_new" command, a "datatype_compat" command, and
+ "primrec_new" command, a "datatype_new_compat" command, and
documentation. See "datatypes.pdf" for details.
- Renamed keywords:
data ~> datatype_new
--- a/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:09:51 2013 +0200
+++ b/src/HOL/BNF/BNF_LFP.thy Fri Aug 30 12:12:41 2013 +0200
@@ -13,7 +13,7 @@
imports BNF_FP_Basic
keywords
"datatype_new" :: thy_decl and
- "datatype_compat" :: thy_decl
+ "datatype_new_compat" :: thy_decl
begin
lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
--- a/src/HOL/BNF/Tools/bnf_fp_n2m.ML Fri Aug 30 12:09:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_n2m.ML Fri Aug 30 12:12:41 2013 +0200
@@ -355,7 +355,7 @@
end;
(* These results are half broken. This is deliberate. We care only about those fields that are
- used by "primrec_new", "primcorec", and "datatype_compat". *)
+ used by "primrec_new", "primcorec", and "datatype_new_compat". *)
val fp_res =
({Ts = fpTs,
bnfs = steal #bnfs,
--- a/src/HOL/BNF/Tools/bnf_lfp_compat.ML Fri Aug 30 12:09:51 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_lfp_compat.ML Fri Aug 30 12:12:41 2013 +0200
@@ -7,7 +7,7 @@
signature BNF_LFP_COMPAT =
sig
- val datatype_compat_cmd : string list -> local_theory -> local_theory
+ val datatype_new_compat_cmd : string list -> local_theory -> local_theory
end;
structure BNF_LFP_Compat : BNF_LFP_COMPAT =
@@ -27,7 +27,7 @@
val compatN = "compat_";
(* TODO: graceful failure for local datatypes -- perhaps by making the command global *)
-fun datatype_compat_cmd raw_fpT_names lthy =
+fun datatype_new_compat_cmd raw_fpT_names lthy =
let
val thy = Proof_Context.theory_of lthy;
@@ -133,8 +133,8 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "datatype_compat"}
+ Outer_Syntax.local_theory @{command_spec "datatype_new_compat"}
"register a new-style datatype as an old-style datatype"
- (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
+ (Scan.repeat1 Parse.type_const >> datatype_new_compat_cmd);
end;