src/HOL/BNF_Def.thy

--- a/src/HOL/BNF_Def.thy	Mon Jan 20 20:42:43 2014 +0100
+++ b/src/HOL/BNF_Def.thy	Mon Jan 20 21:32:41 2014 +0100
@@ -8,9 +8,7 @@
 header {* Definition of Bounded Natural Functors *}
 
 theory BNF_Def
-imports BNF_Util
-   (*FIXME: register fundef_cong attribute in an interpretation to remove this dependency*)
-  FunDef
+imports BNF_Util Fun_Def_Base
 keywords
   "print_bnfs" :: diag and
   "bnf" :: thy_goal