# HG changeset patch
# User haftmann
# Date 1178785308 -7200
# Node ID 3de2d0b5b89ad6abff0d4b7f8b53ab402031c253
# Parent  b8b4d53ccd241ce5acb1ec5d168d82a3e192e61f
explicit import of Datatype.thy due to hook bootstrap problem

diff -r b8b4d53ccd24 -r 3de2d0b5b89a 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")