# HG changeset patch
# User haftmann
# Date 1276504708 -7200
# Node ID 1cf6f134e7f209730d5caa6f4fb128430e01ffa8
# Parent  6c9f23863808483d70310b4374751b4637c61ba9
corrected syntax diagram

diff -r 6c9f23863808 -r 1cf6f134e7f2 doc-src/IsarRef/Thy/HOL_Specific.thy
--- a/doc-src/IsarRef/Thy/HOL_Specific.thy	Sat Jun 12 15:48:17 2010 +0200
+++ b/doc-src/IsarRef/Thy/HOL_Specific.thy	Mon Jun 14 10:38:28 2010 +0200
@@ -1066,7 +1066,7 @@
     target: 'OCaml' | 'SML' | 'Haskell'
     ;
 
-    'code\_datatype' const +
+    'code\_datatype' ( const + )
     ;
 
     'code\_const' (const + 'and') \\
diff -r 6c9f23863808 -r 1cf6f134e7f2 doc-src/IsarRef/Thy/document/HOL_Specific.tex
--- a/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Sat Jun 12 15:48:17 2010 +0200
+++ b/doc-src/IsarRef/Thy/document/HOL_Specific.tex	Mon Jun 14 10:38:28 2010 +0200
@@ -1082,7 +1082,7 @@
     target: 'OCaml' | 'SML' | 'Haskell'
     ;
 
-    'code\_datatype' const +
+    'code\_datatype' ( const + )
     ;
 
     'code\_const' (const + 'and') \\