--- a/src/HOL/ex/Chinese.thy Tue Sep 09 17:51:07 2014 +0200 +++ b/src/HOL/ex/Chinese.thy Tue Sep 09 20:51:36 2014 +0200 @@ -16,7 +16,7 @@ *} -datatype shuzi = +datatype_new shuzi = One ("一") | Two ("二") | Three ("三")