diff -r 3587689271dd -r 789fbbc092d2 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Thu Dec 19 20:07:06 2013 +0100
+++ b/src/Doc/Datatypes/Datatypes.thy	Thu Dec 19 21:49:30 2013 +0100
@@ -467,7 +467,7 @@
 context---e.g., @{text "(in linorder)"}. It is documented in the Isar reference
 manual \cite{isabelle-isar-ref}.
 %
-The optional target is optionally followed by datatype-specific options:
+The optional target is potentially followed by datatype-specific options:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}
@@ -2251,7 +2251,7 @@
   @{syntax_def pcr_formula}: thmdecl? prop (@'of' (term * ))?
 "}
 
-The optional target is optionally followed by a corecursion-specific option:
+The optional target is potentially followed by a corecursion-specific option:
 
 \begin{itemize}
 \setlength{\itemsep}{0pt}