--- a/src/HOL/Recdef.thy Mon Jun 05 14:22:58 2006 +0200
+++ b/src/HOL/Recdef.thy Mon Jun 05 14:26:07 2006 +0200
@@ -6,7 +6,7 @@
header {* TFL: recursive function definitions *}
theory Recdef
-imports Wellfounded_Relations Datatype
+imports Wellfounded_Relations
uses
("../TFL/casesplit.ML")
("../TFL/utils.ML")
@@ -18,7 +18,6 @@
("../TFL/tfl.ML")
("../TFL/post.ML")
("Tools/recdef_package.ML")
- ("Tools/function_package/auto_term.ML")
begin
lemma tfl_eq_True: "(x = True) --> x"
@@ -97,7 +96,4 @@
qed
-use "Tools/function_package/auto_term.ML"
-setup FundefAutoTerm.setup
-
end