--- a/src/HOL/Num.thy Wed Sep 03 00:06:25 2014 +0200
+++ b/src/HOL/Num.thy Wed Sep 03 00:06:26 2014 +0200
@@ -6,7 +6,7 @@
header {* Binary Numerals *}
theory Num
-imports BNF_Least_Fixpoint Old_Datatype
+imports BNF_Least_Fixpoint
begin
subsection {* The @{text num} type *}