1.1 --- a/src/HOL/Enum.thy	Wed Sep 03 00:06:23 2014 +0200
     1.2 +++ b/src/HOL/Enum.thy	Wed Sep 03 00:06:24 2014 +0200
     1.3 @@ -493,7 +493,7 @@
     1.4  
     1.5  text {* We define small finite types for the use in Quickcheck *}
     1.6  
     1.7 -datatype finite_1 = a\<^sub>1
     1.8 +datatype_new finite_1 = a\<^sub>1
     1.9  
    1.10  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.11  
    1.12 @@ -595,7 +595,7 @@
    1.13  declare [[simproc del: finite_1_eq]]
    1.14  hide_const (open) a\<^sub>1
    1.15  
    1.16 -datatype finite_2 = a\<^sub>1 | a\<^sub>2
    1.17 +datatype_new finite_2 = a\<^sub>1 | a\<^sub>2
    1.18  
    1.19  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.20  notation (output) a\<^sub>2  ("a\<^sub>2")
    1.21 @@ -701,7 +701,7 @@
    1.22  
    1.23  hide_const (open) a\<^sub>1 a\<^sub>2
    1.24  
    1.25 -datatype finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    1.26 +datatype_new finite_3 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3
    1.27  
    1.28  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.29  notation (output) a\<^sub>2  ("a\<^sub>2")
    1.30 @@ -825,7 +825,7 @@
    1.31  
    1.32  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3
    1.33  
    1.34 -datatype finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    1.35 +datatype_new finite_4 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4
    1.36  
    1.37  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.38  notation (output) a\<^sub>2  ("a\<^sub>2")
    1.39 @@ -927,7 +927,7 @@
    1.40  hide_const (open) a\<^sub>1 a\<^sub>2 a\<^sub>3 a\<^sub>4
    1.41  
    1.42  
    1.43 -datatype finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    1.44 +datatype_new finite_5 = a\<^sub>1 | a\<^sub>2 | a\<^sub>3 | a\<^sub>4 | a\<^sub>5
    1.45  
    1.46  notation (output) a\<^sub>1  ("a\<^sub>1")
    1.47  notation (output) a\<^sub>2  ("a\<^sub>2")