
diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/ex/Adhoc_Overloading_Examples.thy
--- a/src/HOL/ex/Adhoc_Overloading_Examples.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/ex/Adhoc_Overloading_Examples.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -19,7 +19,7 @@
 subsection {* Plain Ad Hoc Overloading *}
 
 text {*Consider the type of first-order terms.*}
-datatype ('a, 'b) "term" =
+datatype_new ('a, 'b) "term" =
   Var 'b |
   Fun 'a "('a, 'b) term list"
 




