diff -r 414deb2ef328 -r 6fe60a9a5bad src/HOL/Num.thy
--- 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} *}