src/HOL/FunDef.thy

--- a/src/HOL/FunDef.thy	Thu May 10 10:21:47 2007 +0200
+++ b/src/HOL/FunDef.thy	Thu May 10 10:21:48 2007 +0200
@@ -6,7 +6,7 @@
 header {* General recursive function definitions *}
 
 theory FunDef
-imports Accessible_Part
+imports Datatype Accessible_Part
 uses
   ("Tools/function_package/sum_tools.ML")
   ("Tools/function_package/fundef_common.ML")