--- a/src/Doc/Datatypes/Datatypes.thy Mon Feb 17 13:31:42 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Feb 17 13:31:42 2014 +0100
@@ -567,21 +567,21 @@
text {*
\begin{matharray}{rcl}
- @{command_def "datatype_new_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
+ @{command_def "datatype_compat"} & : & @{text "local_theory \<rightarrow> local_theory"}
\end{matharray}
@{rail \<open>
- @@{command datatype_new_compat} (name +)
+ @@{command datatype_compat} (name +)
\<close>}
\medskip
\noindent
-The @{command datatype_new_compat} command registers new-style datatypes as
+The @{command datatype_compat} command registers new-style datatypes as
old-style datatypes. For example:
*}
- datatype_new_compat even_nat odd_nat
+ datatype_compat even_nat odd_nat
text {* \blankline *}
@@ -626,7 +626,7 @@
the old \keyw{primrec} command.
\end{itemize}
-An alternative to @{command datatype_new_compat} is to use the old package's
+An alternative to @{command datatype_compat} is to use the old package's
\keyw{rep\_datatype} command. The associated proof obligations must then be
discharged manually.
*}
@@ -966,7 +966,7 @@
\item \emph{The Standard ML interfaces are different.} Tools and extensions
written to call the old ML interfaces will need to be adapted to the new
interfaces. Little has been done so far in this direction. Whenever possible, it
-is recommended to use @{command datatype_new_compat} or \keyw{rep\_datatype}
+is recommended to use @{command datatype_compat} or \keyw{rep\_datatype}
to register new-style datatypes as old-style datatypes.
\item \emph{The constants @{text t_case} and @{text t_rec} are now called
@@ -1126,12 +1126,12 @@
%
The next example is defined using \keyw{fun} to escape the syntactic
restrictions imposed on primitively recursive functions. The
-@{command datatype_new_compat} command is needed to register new-style datatypes
+@{command datatype_compat} command is needed to register new-style datatypes
for use with \keyw{fun} and \keyw{function}
(Section~\ref{sssec:datatype-new-compat}):
*}
- datatype_new_compat nat
+ datatype_compat nat
text {* \blankline *}
@@ -2714,7 +2714,7 @@
%* partial documentation
%
%* no way to register "sum" and "prod" as (co)datatypes to enable N2M reduction for them
-% (for @{command datatype_new_compat} and prim(co)rec)
+% (for @{command datatype_compat} and prim(co)rec)
%
% * a fortiori, no way to register same type as both data- and codatatype
%
--- a/src/HOL/BNF_Examples/ListF.thy Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/BNF_Examples/ListF.thy Mon Feb 17 13:31:42 2014 +0100
@@ -14,7 +14,7 @@
datatype_new 'a listF (map: mapF rel: relF) =
NilF (defaults tlF: NilF) | Conss (hdF: 'a) (tlF: "'a listF")
-datatype_new_compat listF
+datatype_compat listF
definition Singll ("[[_]]") where
[simp]: "Singll a \<equiv> Conss a NilF"
--- a/src/HOL/BNF_LFP.thy Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/BNF_LFP.thy Mon Feb 17 13:31:42 2014 +0100
@@ -13,7 +13,7 @@
imports BNF_FP_Base
keywords
"datatype_new" :: thy_decl and
- "datatype_new_compat" :: thy_decl
+ "datatype_compat" :: thy_decl
begin
lemma subset_emptyI: "(\<And>x. x \<in> A \<Longrightarrow> False) \<Longrightarrow> A \<subseteq> {}"
--- a/src/HOL/List.thy Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/List.thy Mon Feb 17 13:31:42 2014 +0100
@@ -11,8 +11,7 @@
datatype_new 'a list (map: map rel: list_all2) =
=: Nil (defaults tl: "[]") ("[]")
| Cons (hd: 'a) (tl: "'a list") (infixr "#" 65)
-
-datatype_new_compat list
+datatype_compat list
lemma [case_names Nil Cons, cases type: list]:
-- {* for backward compatibility -- names of variables differ *}
--- a/src/HOL/Option.thy Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Option.thy Mon Feb 17 13:31:42 2014 +0100
@@ -11,8 +11,7 @@
datatype_new 'a option =
=: None
| Some (the: 'a)
-
-datatype_new_compat option
+datatype_compat option
lemma [case_names None Some, cases type: option]:
-- {* for backward compatibility -- names of variables differ *}
--- a/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m.ML Mon Feb 17 13:31:42 2014 +0100
@@ -355,7 +355,7 @@
end;
(* These results are half broken. This is deliberate. We care only about those fields that are
- used by "primrec", "primcorecursive", and "datatype_new_compat". *)
+ used by "primrec", "primcorecursive", and "datatype_compat". *)
val fp_res =
({Ts = fpTs,
bnfs = steal #bnfs,
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Mon Feb 17 13:31:42 2014 +0100
@@ -7,7 +7,7 @@
signature BNF_LFP_COMPAT =
sig
- val datatype_new_compat_cmd : string list -> local_theory -> local_theory
+ val datatype_compat_cmd : string list -> local_theory -> local_theory
end;
structure BNF_LFP_Compat : BNF_LFP_COMPAT =
@@ -24,7 +24,7 @@
val code_nitpicksimp_simp_attrs = Code.add_default_eqn_attrib :: @{attributes [nitpick_simp, simp]};
(* TODO: graceful failure for local datatypes -- perhaps by making the command global *)
-fun datatype_new_compat_cmd raw_fpT_names lthy =
+fun datatype_compat_cmd raw_fpT_names lthy =
let
val thy = Proof_Context.theory_of lthy;
@@ -203,8 +203,8 @@
end;
val _ =
- Outer_Syntax.local_theory @{command_spec "datatype_new_compat"}
+ Outer_Syntax.local_theory @{command_spec "datatype_compat"}
"register new-style datatypes as old-style datatypes"
- (Scan.repeat1 Parse.type_const >> datatype_new_compat_cmd);
+ (Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
end;