diff -r 58d1b63bea81 -r 4163160853fd src/Doc/Datatypes/Datatypes.thy
--- a/src/Doc/Datatypes/Datatypes.thy	Mon Sep 23 14:53:43 2013 +0200
+++ b/src/Doc/Datatypes/Datatypes.thy	Mon Sep 23 17:43:23 2013 +0200
@@ -764,7 +764,7 @@
 @{thm list.discI(1)[no_vars]} \\
 @{thm list.discI(2)[no_vars]}
 
-\item[@{text "t."}\hthm{sel} @{text "[simp]"}\rm:] ~ \\
+\item[@{text "t."}\hthm{sel} @{text "[simp, code]"}\rm:] ~ \\
 @{thm list.sel(1)[no_vars]} \\
 @{thm list.sel(2)[no_vars]}