# HG changeset patch
# User blanchet
# Date 1376313917 -7200
# Node ID f2df0730f8ac3fc45ddb84517487b732cba3d0cf
# Parent  2b430bbb5a1af34bf7326f4090ce29a06801951d
clarified option name (since case/fold/rec are also destructors)

diff -r 2b430bbb5a1a -r f2df0730f8ac src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Aug 12 15:25:17 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Aug 12 15:25:17 2013 +0200
@@ -411,7 +411,7 @@
   @@{command datatype_new} @{syntax target}? @{syntax dt_options}? \\
     (@{syntax dt_name} '=' (@{syntax ctor} + '|') + @'and')
   ;
-  @{syntax_def dt_options}: '(' ((@'no_dests' | @'rep_compat') + ',') ')'
+  @{syntax_def dt_options}: '(' ((@'no_discs_sels' | @'rep_compat') + ',') ')'
 "}
 
 The syntactic quantity @{syntax target} can be used to specify a local context
@@ -424,7 +424,7 @@
 \setlength{\itemsep}{0pt}
 
 \item
-The \keyw{no\_dests} option indicates that no destructors (i.e.,
+The \keyw{no\_discs\_sels} option indicates that no destructors (i.e.,
 discriminators and selectors) should be generated.
 
 \item
@@ -888,7 +888,7 @@
 text {*
 Definitions of codatatypes have almost exactly the same syntax as for datatypes
 (Section~\ref{ssec:datatype-syntax}), with two exceptions: The command is called
-@{command codatatype}; the \keyw{no\_dests} option is not available, because
+@{command codatatype}; the \keyw{no\_discs\_sels} option is not available, because
 destructors are a central notion for codatatypes.
 *}
 
@@ -982,7 +982,8 @@
     old @{command datatype}
 
   * @{command wrap_free_constructors}
-    * \keyw{no\_dests}, \keyw{rep\_compat}
+    * \keyw{no\_discs\_sels}, \keyw{rep\_compat}
+    * hack to have both co and nonco view via locale (cf. ext nats)
 *}
 
 
diff -r 2b430bbb5a1a -r f2df0730f8ac src/HOL/BNF/BNF_Ctr_Sugar.thy
--- a/src/HOL/BNF/BNF_Ctr_Sugar.thy	Mon Aug 12 15:25:17 2013 +0200
+++ b/src/HOL/BNF/BNF_Ctr_Sugar.thy	Mon Aug 12 15:25:17 2013 +0200
@@ -11,7 +11,7 @@
 imports BNF_Util
 keywords
   "wrap_free_constructors" :: thy_goal and
-  "no_dests" and
+  "no_discs_sels" and
   "rep_compat"
 begin
 
diff -r 2b430bbb5a1a -r f2df0730f8ac src/HOL/BNF/Tools/bnf_ctr_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Aug 12 15:25:17 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_ctr_sugar.ML	Mon Aug 12 15:25:17 2013 +0200
@@ -177,7 +177,7 @@
 
 fun eta_expand_arg xs f_xs = fold_rev Term.lambda xs f_xs;
 
-fun prepare_wrap_free_constructors prep_term ((((no_dests, rep_compat), raw_ctrs),
+fun prepare_wrap_free_constructors prep_term ((((no_discs_sels, rep_compat), raw_ctrs),
     raw_case_binding), (raw_disc_bindings, (raw_sel_bindingss, raw_sel_defaultss))) no_defs_lthy =
   let
     (* TODO: sanity checks on arguments *)
@@ -335,7 +335,7 @@
 
     val (all_sels_distinct, discs, selss, udiscs, uselss, vdiscs, vselss, disc_defs, sel_defs,
          sel_defss, lthy') =
-      if no_dests then
+      if no_discs_sels then
         (true, [], [], [], [], [], [], [], [], [], lthy)
       else
         let
@@ -504,7 +504,7 @@
 
         val (all_sel_thms, sel_thmss, disc_thmss, disc_thms, discI_thms, disc_exclude_thms,
              disc_exhaust_thms, collapse_thms, expand_thms, case_conv_thms) =
-          if no_dests then
+          if no_discs_sels then
             ([], [], [], [], [], [], [], [], [], [])
           else
             let
@@ -790,7 +790,7 @@
 val parse_bound_termss = parse_bracket_list parse_bound_terms;
 
 val parse_wrap_free_constructors_options =
-  Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_dests"} >> K (true, false)) ||
+  Scan.optional (@{keyword "("} |-- Parse.list1 ((@{keyword "no_discs_sels"} >> K (true, false)) ||
       (@{keyword "rep_compat"} >> K (false, true))) --| @{keyword ")"}
     >> (pairself (exists I) o split_list)) (false, false);
 
diff -r 2b430bbb5a1a -r f2df0730f8ac src/HOL/BNF/Tools/bnf_fp_def_sugar.ML
--- a/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Aug 12 15:25:17 2013 +0200
+++ b/src/HOL/BNF/Tools/bnf_fp_def_sugar.ML	Mon Aug 12 15:25:17 2013 +0200
@@ -953,12 +953,12 @@
   end;
 
 fun define_co_datatypes prepare_constraint prepare_typ prepare_term fp construct_fp
-    (wrap_opts as (no_dests, rep_compat), specs) no_defs_lthy0 =
+    (wrap_opts as (no_discs_sels, rep_compat), specs) no_defs_lthy0 =
   let
     (* TODO: sanity checks on arguments *)
 
-    val _ = if fp = Greatest_FP andalso no_dests then
-        error "Cannot define destructor-less codatatypes"
+    val _ = if fp = Greatest_FP andalso no_discs_sels then
+        error "Cannot define codatatypes without discriminators and selectors"
       else
         ();