--- 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)
*}
--- 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
--- 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);
--- 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
();