--- a/src/HOL/Num.thy Wed Sep 03 00:06:23 2014 +0200
+++ b/src/HOL/Num.thy Wed Sep 03 00:06:24 2014 +0200
@@ -11,7 +11,7 @@
subsection {* The @{text num} type *}
-datatype num = One | Bit0 num | Bit1 num
+datatype_new num = One | Bit0 num | Bit1 num
text {* Increment function for type @{typ num} *}