--- a/src/HOL/Num.thy Thu Sep 11 19:26:59 2014 +0200
+++ b/src/HOL/Num.thy Thu Sep 11 19:32:36 2014 +0200
@@ -11,7 +11,7 @@
subsection {* The @{text num} type *}
-datatype_new num = One | Bit0 num | Bit1 num
+datatype num = One | Bit0 num | Bit1 num
text {* Increment function for type @{typ num} *}