diff -r a09ec6daaa19 -r 91ea607a34d8 src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Thu Sep 11 19:32:36 2014 +0200
@@ -19,7 +19,7 @@
 subsection {* Plain Ad Hoc Overloading *}
 
 text {*Consider the type of first-order terms.*}
-datatype_new ('a, 'b) "term" =
+datatype ('a, 'b) "term" =
   Var 'b |
   Fun 'a "('a, 'b) term list"