--- a/src/HOL/Library/Countable.thy Thu Sep 11 19:41:45 2014 +0200
+++ b/src/HOL/Library/Countable.thy Thu Sep 11 19:45:42 2014 +0200
@@ -197,7 +197,7 @@
hide_const (open) finite_item nth_item
-subsection {* Automatically proving countability of new-style datatypes *}
+subsection {* Automatically proving countability of datatypes *}
ML_file "bnf_lfp_countable.ML"
--- a/src/HOL/Library/bnf_lfp_countable.ML Thu Sep 11 19:41:45 2014 +0200
+++ b/src/HOL/Library/bnf_lfp_countable.ML Thu Sep 11 19:45:42 2014 +0200
@@ -125,9 +125,8 @@
fun derive_encode_injectives_thms _ [] = []
| derive_encode_injectives_thms ctxt fpT_names0 =
let
- fun not_datatype s = error (quote s ^ " is not a new-style datatype");
- fun not_mutually_recursive ss =
- error (commas ss ^ " are not mutually recursive new-style datatypes");
+ fun not_datatype s = error (quote s ^ " is not a datatype");
+ fun not_mutually_recursive ss = error (commas ss ^ " are not mutually recursive datatypes");
fun lfp_sugar_of s =
(case fp_sugar_of ctxt s of
--- a/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Sep 11 19:41:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML Thu Sep 11 19:45:42 2014 +0200
@@ -341,7 +341,7 @@
fun not_co_datatype (T as Type (s, _)) =
if fp = Least_FP andalso
is_some (Old_Datatype_Data.get_info (Proof_Context.theory_of lthy) s) then
- error (qsoty T ^ " is not a new-style datatype (cf. \"datatype\")")
+ error (qsoty T ^ " is an old-style datatype")
else
not_co_datatype0 T
| not_co_datatype T = not_co_datatype0 T;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 11 19:41:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Thu Sep 11 19:45:42 2014 +0200
@@ -3,7 +3,7 @@
Author: Andrei Popescu, TU Muenchen
Copyright 2012
-New-style datatype construction.
+Datatype construction.
*)
signature BNF_LFP =
--- a/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Sep 11 19:41:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_compat.ML Thu Sep 11 19:45:42 2014 +0200
@@ -210,9 +210,9 @@
let
val thy = Proof_Context.theory_of lthy;
- fun not_datatype s = error (quote s ^ " is not a new-style datatype");
+ fun not_datatype s = error (quote s ^ " is not a datatype");
fun not_mutually_recursive ss =
- error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive new-style datatypes");
+ error ("{" ^ commas ss ^ "} is not a complete set of mutually recursive datatypes");
fun lfp_sugar_of s =
(case fp_sugar_of lthy s of
@@ -528,7 +528,7 @@
val _ =
Outer_Syntax.local_theory @{command_spec "datatype_compat"}
- "register new-style datatypes as old-style datatypes"
+ "register datatypes as old-style datatypes and derive old-style properties"
(Scan.repeat1 Parse.type_const >> datatype_compat_cmd);
end;
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Sep 11 19:41:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML Thu Sep 11 19:45:42 2014 +0200
@@ -3,7 +3,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2013
-New-style recursor sugar ("primrec").
+Recursor sugar ("primrec").
*)
signature BNF_LFP_REC_SUGAR =
--- a/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Sep 11 19:41:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML Thu Sep 11 19:45:42 2014 +0200
@@ -3,7 +3,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2013
-More new-style recursor sugar.
+More recursor sugar.
*)
structure BNF_LFP_Rec_Sugar_More : sig end =
--- a/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 11 19:41:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_size.ML Thu Sep 11 19:45:42 2014 +0200
@@ -2,7 +2,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2014
-Generation of size functions for new-style datatypes.
+Generation of size functions for datatypes.
*)
signature BNF_LFP_SIZE =
--- a/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Sep 11 19:41:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_tactics.ML Thu Sep 11 19:45:42 2014 +0200
@@ -3,7 +3,7 @@
Author: Andrei Popescu, TU Muenchen
Copyright 2012
-Tactics for the new-style datatype construction.
+Tactics for the datatype construction.
*)
signature BNF_LFP_TACTICS =
--- a/src/HOL/Tools/BNF/bnf_lfp_util.ML Thu Sep 11 19:41:45 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_lfp_util.ML Thu Sep 11 19:45:42 2014 +0200
@@ -3,7 +3,7 @@
Author: Jasmin Blanchette, TU Muenchen
Copyright 2012
-Library for the new-style datatype construction.
+Library for the datatype construction.
*)
signature BNF_LFP_UTIL =