# HG changeset patch
# User traytel
# Date 1485189337 -3600
# Node ID c8626f7fae060cdc4706c223217d520639575ca7
# Parent  1b584fab241a728fa3ea1dbe72c1bef08bb7d086
tuned documentation

diff -r 1b584fab241a -r c8626f7fae06 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Sun Jan 22 19:37:06 2017 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Jan 23 17:35:37 2017 +0100
@@ -477,9 +477,9 @@
   @{syntax_def plugins}: 'plugins' ('only' | 'del') ':' (name +)
   ;
   @{syntax_def dt_spec}: (@{syntax dt_name} '=' (@{syntax dt_ctor} + '|') \<newline>
-     @{syntax map_rel}? (@'where' (prop + '|'))? + @'and')
+     @{syntax map_rel_pred}? (@'where' (prop + '|'))? + @'and')
   ;
-  @{syntax_def map_rel}: @'for' ((('map' | 'rel') ':' name) +)
+  @{syntax_def map_rel_pred}: @'for' ((('map' | 'rel' | 'pred') ':' name) +)
 \<close>}
 
 \medskip
@@ -3020,7 +3020,7 @@
 @{rail \<open>
   @@{command lift_bnf} target? lb_options? \<newline>
     @{syntax tyargs} name wit_terms?  \<newline>
-    ('via' thm)? @{syntax map_rel}?
+    ('via' thm)? @{syntax map_rel_pred}?
   ;
   @{syntax_def lb_options}: '(' ((@{syntax plugins} | 'no_warn_wits') + ',') ')'
   ;
@@ -3055,7 +3055,7 @@
 
 @{rail \<open>
   @@{command copy_bnf} target? ('(' @{syntax plugins} ')')? \<newline>
-    @{syntax tyargs} name ('via' thm)? @{syntax map_rel}?
+    @{syntax tyargs} name ('via' thm)? @{syntax map_rel_pred}?
 \<close>}
 \medskip
 
@@ -3077,7 +3077,7 @@
 @{rail \<open>
   @@{command bnf_axiomatization} target? ('(' @{syntax plugins} ')')? \<newline>
     @{syntax tyargs}? name @{syntax wit_types}? \<newline>
-    mixfix? @{syntax map_rel}?
+    mixfix? @{syntax map_rel_pred}?
   ;
   @{syntax_def wit_types}: '[' 'wits' ':' types ']'
 \<close>}