# HG changeset patch
# User blanchet
# Date 1410457542 -7200
# Node ID 6d8458bc6e27987229d8ebf6a9ca75da2f70e128
# Parent  ee1be8b3032e6270fda0233191f736f4b717d689
tuning terminology

diff -r ee1be8b3032e -r 6d8458bc6e27 src/HOL/Library/Countable.thy
--- 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"
 
diff -r ee1be8b3032e -r 6d8458bc6e27 src/HOL/Library/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
diff -r ee1be8b3032e -r 6d8458bc6e27 src/HOL/Tools/BNF/bnf_fp_n2m_sugar.ML
--- 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;
diff -r ee1be8b3032e -r 6d8458bc6e27 src/HOL/Tools/BNF/bnf_lfp.ML
--- 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 =
diff -r ee1be8b3032e -r 6d8458bc6e27 src/HOL/Tools/BNF/bnf_lfp_compat.ML
--- 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;
diff -r ee1be8b3032e -r 6d8458bc6e27 src/HOL/Tools/BNF/bnf_lfp_rec_sugar.ML
--- 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 =
diff -r ee1be8b3032e -r 6d8458bc6e27 src/HOL/Tools/BNF/bnf_lfp_rec_sugar_more.ML
--- 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 =
diff -r ee1be8b3032e -r 6d8458bc6e27 src/HOL/Tools/BNF/bnf_lfp_size.ML
--- 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 =
diff -r ee1be8b3032e -r 6d8458bc6e27 src/HOL/Tools/BNF/bnf_lfp_tactics.ML
--- 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 =
diff -r ee1be8b3032e -r 6d8458bc6e27 src/HOL/Tools/BNF/bnf_lfp_util.ML
--- 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 =