# HG changeset patch
# User blanchet
# Date 1401114786 -7200
# Node ID 59603f4f1d2ec36708923e42a211a83cbc0f49b4
# Parent  1fa9c19ba2c9269dff764efadc523e057dac897a
changed '-:' to 'dead' in BNF

diff -r 1fa9c19ba2c9 -r 59603f4f1d2e src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon May 26 16:32:55 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon May 26 16:33:06 2014 +0200
@@ -505,7 +505,7 @@
 @{rail \<open>
   @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
   ;
-  @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
+  @{syntax_def tyargs}: typefree | '(' (('dead' | name ':')? typefree + ',') ')'
   ;
   @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
 \<close>}
@@ -519,8 +519,8 @@
 
 The optional names preceding the type variables allow to override the default
 names of the set functions (@{text set1_t}, \ldots, @{text setM_t}). Type
-arguments can be marked as dead by entering ``@{text "-"}'' (hyphen) instead of an
-identifier for the corresponding set function; otherwise, they are live or dead
+arguments can be marked as dead by entering ``@{text dead}'' in front of the
+type variable (e.g., ``@{text "(dead 'a)"}''); otherwise, they are live or dead
 (and a set function is generated or not) depending on where they occur in the
 right-hand sides of the definition. Declaring a type argument as dead can speed
 up the type definition but will prevent any later (co)recursion through that
@@ -2572,10 +2572,11 @@
 parenthesized mixfix notation \cite{isabelle-isar-ref}.
 
 Type arguments are live by default; they can be marked as dead by entering
-``-'' (hyphen) instead of an identifier for the corresponding set function.
-Witnesses can be specified by their types. Otherwise, the syntax of
-@{command bnf_axiomatization} is identical to the left-hand side of a
-@{command datatype_new} or @{command codatatype} definition.
+``@{text dead}'' in front of the type variable (e.g., ``@{text "(dead 'a)"}'')
+instead of an identifier for the corresponding set function. Witnesses can be
+specified by their types. Otherwise, the syntax of @{command bnf_axiomatization}
+is identical to the left-hand side of a @{command datatype_new} or
+@{command codatatype} definition.
 
 The command is useful to reason abstractly about BNFs. The axioms are safe
 because there exists BNFs of arbitrary large arities. Applications must import
diff -r 1fa9c19ba2c9 -r 59603f4f1d2e src/HOL/Tools/BNF/bnf_util.ML
--- a/src/HOL/Tools/BNF/bnf_util.ML	Mon May 26 16:32:55 2014 +0200
+++ b/src/HOL/Tools/BNF/bnf_util.ML	Mon May 26 16:33:06 2014 +0200
@@ -290,7 +290,7 @@
   Parse.type_ident -- Scan.option (@{keyword "::"} |-- Parse.!!! Parse.sort);
 
 val parse_type_arg_named_constrained =
-   (Parse.minus --| @{keyword ":"} >> K NONE || parse_opt_binding_colon >> SOME) --
+   (Parse.reserved "dead" >> K NONE || parse_opt_binding_colon >> SOME) --
    parse_type_arg_constrained;
 
 val parse_type_args_named_constrained =