diff -r 25af24e1f37b -r 180f1b3508ed src/HOL/Library/Lattice_Constructions.thy
--- a/src/HOL/Library/Lattice_Constructions.thy	Tue Sep 09 17:51:07 2014 +0200
+++ b/src/HOL/Library/Lattice_Constructions.thy	Tue Sep 09 20:51:36 2014 +0200
@@ -9,7 +9,7 @@
 
 subsection {* Values extended by a bottom element *}
 
-datatype 'a bot = Value 'a | Bot
+datatype_new 'a bot = Value 'a | Bot
 
 instantiation bot :: (preorder) preorder
 begin
@@ -108,7 +108,7 @@
 
 section {* Values extended by a top element *}
 
-datatype 'a top = Value 'a | Top
+datatype_new 'a top = Value 'a | Top
 
 instantiation top :: (preorder) preorder
 begin
@@ -207,7 +207,7 @@
 
 subsection {* Values extended by a top and a bottom element *}
 
-datatype 'a flat_complete_lattice = Value 'a | Bot | Top
+datatype_new 'a flat_complete_lattice = Value 'a | Bot | Top
 
 instantiation flat_complete_lattice :: (type) order
 begin