diff -r a09ec6daaa19 -r 91ea607a34d8 src/Doc/Functions/Functions.thy
--- a/src/Doc/Functions/Functions.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/Doc/Functions/Functions.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -522,7 +522,7 @@
   and @{term "X"} for true, false and uncertain propositions, respectively. 
 *}
 
-datatype_new P3 = T | F | X
+datatype P3 = T | F | X
 
 text {* \noindent Then the conjunction of such values can be defined as follows: *}
 
@@ -1122,7 +1122,7 @@
   As an example, imagine a datatype of n-ary trees:
 *}
 
-datatype_new 'a tree = 
+datatype 'a tree = 
   Leaf 'a 
 | Branch "'a tree list"