# HG changeset patch
# User blanchet
# Date 1377857561 -7200
# Node ID 42a99f732a409347008ebf6ad2063ede3dca2156
# Parent  d066e4923a315168daba722d7af39414c72a7408
renamed command to clarify connection with BNF

diff -r d066e4923a31 -r 42a99f732a40 NEWS
--- 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
diff -r d066e4923a31 -r 42a99f732a40 src/HOL/BNF/BNF_LFP.thy
--- 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> {}"
diff -r d066e4923a31 -r 42a99f732a40 src/HOL/BNF/Tools/bnf_fp_n2m.ML
--- 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,
diff -r d066e4923a31 -r 42a99f732a40 src/HOL/BNF/Tools/bnf_lfp_compat.ML
--- 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;