--- a/src/HOL/Library/Lattice_Constructions.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Library/Lattice_Constructions.thy Thu Sep 11 19:32:36 2014 +0200
@@ -9,7 +9,7 @@
subsection {* Values extended by a bottom element *}
-datatype_new 'a bot = Value 'a | Bot
+datatype 'a bot = Value 'a | Bot
instantiation bot :: (preorder) preorder
begin
@@ -108,7 +108,7 @@
section {* Values extended by a top element *}
-datatype_new 'a top = Value 'a | Top
+datatype '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_new 'a flat_complete_lattice = Value 'a | Bot | Top
+datatype 'a flat_complete_lattice = Value 'a | Bot | Top
instantiation flat_complete_lattice :: (type) order
begin