--- a/src/HOL/FunDef.thy Thu Dec 06 12:23:52 2007 +0100
+++ b/src/HOL/FunDef.thy Thu Dec 06 12:58:01 2007 +0100
@@ -13,6 +13,7 @@
("Tools/function_package/inductive_wrap.ML")
("Tools/function_package/context_tree.ML")
("Tools/function_package/fundef_core.ML")
+ ("Tools/function_package/sum_tree.ML")
("Tools/function_package/mutual.ML")
("Tools/function_package/pattern_split.ML")
("Tools/function_package/fundef_package.ML")
@@ -98,6 +99,7 @@
use "Tools/function_package/inductive_wrap.ML"
use "Tools/function_package/context_tree.ML"
use "Tools/function_package/fundef_core.ML"
+use "Tools/function_package/sum_tree.ML"
use "Tools/function_package/mutual.ML"
use "Tools/function_package/pattern_split.ML"
use "Tools/function_package/auto_term.ML"