# HG changeset patch
# User blanchet
# Date 1393192271 -3600
# Node ID a98a045a61699a45ffa7bbc502118729a95ad422
# Parent  a97b9b81e19506e59e28506091934bcabfeddffa
updated docs

diff -r a97b9b81e195 -r a98a045a6169 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Sun Feb 23 22:51:11 2014 +0100
@@ -501,7 +501,7 @@
 @{rail \<open>
   @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? mixfix?
   ;
-  @{syntax_def tyargs}: typefree | '(' ((name ':')? typefree + ',') ')'
+  @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
   ;
   @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
 \<close>}
@@ -514,7 +514,14 @@
 variable (@{typ 'a}, @{typ 'b}, \ldots) \cite{isabelle-isar-ref}.
 
 The optional names preceding the type variables allow to override the default
-names of the set functions (@{text set1_t}, \ldots, @{text setM_t}).
+names of the set functions (@{text set1_t}, \ldots, @{text setM_t}). Type
+arguments can be marked as dead by entering ``-'' (hyphen) instead of an
+identifier for the corresponding set function; 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
+type argument.
+
 Inside a mutually recursive specification, all defined datatypes must
 mention exactly the same type variables in the same order.
 
@@ -2530,15 +2537,9 @@
 \end{matharray}
 
 @{rail \<open>
-  @@{command bnf_decl} target? @{syntax dt_name}
-  ;
-  @{syntax_def dt_name}: @{syntax tyargs}? name @{syntax map_rel}? \<newline>
+  @@{command bnf_decl} target? @{syntax tyargs}? name @{syntax map_rel}? \<newline>
     @{syntax wit_types}? mixfix?
   ;
-  @{syntax_def tyargs}: typefree | '(' (((name | '-') ':')? typefree + ',') ')'
-  ;
-  @{syntax_def map_rel}: '(' ((('map' | 'rel') ':' name) +) ')'
-  ;
   @{syntax_def wit_types}: '[' 'wits' ':' types ']'
 \<close>}
 
diff -r a97b9b81e195 -r a98a045a6169 src/HOL/BNF_Comp.thy
--- a/src/HOL/BNF_Comp.thy	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/BNF_Comp.thy	Sun Feb 23 22:51:11 2014 +0100
@@ -68,7 +68,7 @@
 unfolding Grp_def fun_eq_iff relcompp.simps by auto
 
 lemma OO_Grp_cong: "A = B \<Longrightarrow> (Grp A f)^--1 OO Grp A g = (Grp B f)^--1 OO Grp B g"
-by simp
+by (rule arg_cong)
 
 ML_file "Tools/BNF/bnf_comp_tactics.ML"
 ML_file "Tools/BNF/bnf_comp.ML"
diff -r a97b9b81e195 -r a98a045a6169 src/HOL/Tools/BNF/bnf_comp.ML
--- a/src/HOL/Tools/BNF/bnf_comp.ML	Sun Feb 23 22:51:11 2014 +0100
+++ b/src/HOL/Tools/BNF/bnf_comp.ML	Sun Feb 23 22:51:11 2014 +0100
@@ -660,7 +660,7 @@
       fun check_bad_dead ((_, (deads, _)), _) =
         let val Ds = fold Term.add_tfreesT deads [] in
           (case Library.inter (op =) Ds Xs of [] => ()
-           | X :: _ => raise BAD_DEAD (TFree X, T))
+          | X :: _ => raise BAD_DEAD (TFree X, T))
         end;
 
       val tfrees = subtract (op =) Ds0 (Term.add_tfreesT T []);