src/HOL/FunDef.thy

 *)
 
 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")
   ("Tools/function_package/inductive_wrap.ML")
   ("Tools/function_package/context_tree.ML")

   ("Tools/function_package/mutual.ML")
   ("Tools/function_package/pattern_split.ML")
   ("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. *}
 
 definition

 use "Tools/function_package/mutual.ML"
 use "Tools/function_package/pattern_split.ML"
 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]:
   "M = N \<Longrightarrow> (\<And>x. x = N \<Longrightarrow> f x = g x) \<Longrightarrow> Let M f = Let N g"
   unfolding Let_def by blast