
diff -r c95319d14332 -r be61bd159a99 src/HOL/FunDef.thy
--- 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"




