diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Enum.thy	Wed Sep 03 00:06:24 2014 +0200
@@ -493,7 +493,7 @@
 
 text {* We define small finite types for the use in Quickcheck *}
 
-datatype finite_1 = a\<^sub>1
+datatype_new finite_1 = a\<^sub>1
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 
@@ -595,7 +595,7 @@
 declare [[simproc del: finite_1_eq]]
 hide_const (open) a\<^sub>1
 
-datatype finite_2 = a\<^sub>1 | a\<^sub>2
+datatype_new finite_2 = a\<^sub>1 | a\<^sub>2
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
@@ -701,7 +701,7 @@
 
 hide_const (open) a\<^sub>1 a\<^sub>2
 
-datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
+datatype_new finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
@@ -825,7 +825,7 @@
 
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
 
-datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
+datatype_new finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")
@@ -927,7 +927,7 @@
 hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
 
 
-datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
+datatype_new finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
 
 notation (output) a\<^sub>1  ("a\<^sub>1")
 notation (output) a\<^sub>2  ("a\<^sub>2")