--- a/src/HOL/FunDef.thy Thu Feb 15 12:14:34 2007 +0100
+++ b/src/HOL/FunDef.thy Thu Feb 15 17:35:19 2007 +0100
@@ -14,7 +14,6 @@
("Tools/function_package/inductive_wrap.ML")
("Tools/function_package/context_tree.ML")
("Tools/function_package/fundef_core.ML")
-("Tools/function_package/termination.ML")
("Tools/function_package/mutual.ML")
("Tools/function_package/pattern_split.ML")
("Tools/function_package/fundef_package.ML")
@@ -109,7 +108,6 @@
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/termination.ML"
use "Tools/function_package/mutual.ML"
use "Tools/function_package/pattern_split.ML"
use "Tools/function_package/auto_term.ML"