# HG changeset patch
# User blanchet
# Date 1410774887 -7200
# Node ID f6af48bd7c04e65ab596d7adff9dc3bdf7b9dbb5
# Parent  d109244b89aa29d996d9e92d8034ce1c3cfdd795
more hints on how to port 'size'

diff -r d109244b89aa -r f6af48bd7c04 src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 15 11:37:55 2014 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 15 11:54:47 2014 +0200
@@ -1069,6 +1069,10 @@
 The new function returns @{text 1} instead of @{text 0} for some nonrecursive
 constructors. This departure from the old behavior made it possible to implement
 @{const size} in terms of the parameterized function @{text "t.size_t"}.
+Moreover, the new function considers nested occurrences of a value, in the nested
+recursive case. The old behavior can be obtained by disabling the @{text size}
+plugin (Section~\ref{sec:controlling-plugins}) and instantiating the
+@{text size} type class manually.
 
 \item \emph{The internal constructions are completely different.} Proof texts
 that unfold the definition of constants introduced by \keyw{old_datatype} will