src/HOL/FunDef.thy

--- a/src/HOL/FunDef.thy	Thu Apr 24 16:53:04 2008 +0200
+++ b/src/HOL/FunDef.thy	Fri Apr 25 15:30:33 2008 +0200
@@ -6,7 +6,7 @@
 header {* General recursive function definitions *}
 
 theory FunDef
-imports Accessible_Part
+imports Wellfounded
 uses
   ("Tools/function_package/fundef_lib.ML")
   ("Tools/function_package/fundef_common.ML")
@@ -19,6 +19,8 @@
   ("Tools/function_package/fundef_package.ML")
   ("Tools/function_package/auto_term.ML")
   ("Tools/function_package/induction_scheme.ML")
+  ("Tools/function_package/lexicographic_order.ML")
+  ("Tools/function_package/fundef_datatype.ML")
 begin
 
 text {* Definitions with default value. *}
@@ -106,10 +108,14 @@
 use "Tools/function_package/auto_term.ML"
 use "Tools/function_package/fundef_package.ML"
 use "Tools/function_package/induction_scheme.ML"
+use "Tools/function_package/lexicographic_order.ML"
+use "Tools/function_package/fundef_datatype.ML"
 
 setup {* 
   FundefPackage.setup 
   #> InductionScheme.setup
+  #> LexicographicOrder.setup 
+  #> FundefDatatype.setup
 *}
 
 lemma let_cong [fundef_cong]: