# 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: "(\x. x \ A \ False) \ A \ {}" 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;