diff -r 6260caf1d612 -r b18bdcbda41b src/HOL/Num.thy
--- a/src/HOL/Num.thy	Mon Feb 17 13:31:42 2014 +0100
+++ b/src/HOL/Num.thy	Mon Feb 17 13:31:42 2014 +0100
@@ -6,7 +6,7 @@
 header {* Binary Numerals *}
 
 theory Num
-imports Datatype
+imports Datatype BNF_LFP
 begin
 
 subsection {* The @{text num} type *}
@@ -1249,4 +1249,3 @@
   code_module Num \<rightharpoonup> (SML) Arith and (OCaml) Arith and (Haskell) Arith
 
 end
-