--- a/src/Doc/Datatypes/Datatypes.thy Mon Sep 08 14:03:01 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy Mon Sep 08 14:03:02 2014 +0200
@@ -615,7 +615,8 @@
\item The old-style, nested-as-mutual induction rule and recursor theorems are
generated under their usual names but with ``@{text "compat_"}'' prefixed
-(e.g., @{text compat_tree.induct}).
+(e.g., @{text compat_tree.induct}, @{text compat_tree.inducts}, and
+@{text compat_tree.rec}).
\item All types through which recursion takes place must be new-style datatypes
or the function type. In principle, it should be possible to support old-style