--- a/src/Doc/Datatypes/Datatypes.thy Tue May 05 16:52:09 2015 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Wed May 06 14:23:22 2015 +0200
@@ -169,7 +169,7 @@
text {*
Datatypes are illustrated through concrete examples featuring different flavors
of recursion. More examples can be found in the directory
-\verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|.
+\verb|~~/src/HOL/|\allowbreak\verb|Datatype_Examples|.
*}
@@ -1675,7 +1675,7 @@
Codatatypes can be specified using the @{command codatatype} command. The
command is first illustrated through concrete examples featuring different
flavors of corecursion. More examples can be found in the directory
-\verb|~~/src/HOL/|\allowbreak\verb|BNF/Examples|. The
+\verb|~~/src/HOL/|\allowbreak\verb|Datatype_Examples|. The
\emph{Archive of Formal Proofs} also includes some useful codatatypes, notably
for lazy lists @{cite "lochbihler-2010"}.
*}