src/HOL/Recdef.thy

--- a/src/HOL/Recdef.thy	Fri May 05 16:50:58 2006 +0200
+++ b/src/HOL/Recdef.thy	Fri May 05 17:17:21 2006 +0200
@@ -18,6 +18,7 @@
   ("../TFL/tfl.ML")
   ("../TFL/post.ML")
   ("Tools/recdef_package.ML")
+  ("Tools/function_package/auto_term.ML")
 begin
 
 lemma tfl_eq_True: "(x = True) --> x"
@@ -95,4 +96,8 @@
   finally show "finite (UNIV :: 'a option set)" .
 qed
 
+
+use "Tools/function_package/auto_term.ML"
+setup FundefAutoTerm.setup
+
 end