diff -r 33d44b1520c0 -r bc0cea4cae52 src/HOL/FunDef.thy
--- a/src/HOL/FunDef.thy	Sat Jan 02 22:57:19 2010 +0100
+++ b/src/HOL/FunDef.thy	Sat Jan 02 23:18:58 2010 +0100
@@ -24,8 +24,6 @@
   ("Tools/Function/fun.ML")
   ("Tools/Function/induction_schema.ML")
   ("Tools/Function/termination.ML")
-  ("Tools/Function/decompose.ML")
-  ("Tools/Function/descent.ML")
   ("Tools/Function/scnp_solve.ML")
   ("Tools/Function/scnp_reconstruct.ML")
 begin
@@ -309,8 +307,6 @@
 subsection {* Tool setup *}
 
 use "Tools/Function/termination.ML"
-use "Tools/Function/decompose.ML"
-use "Tools/Function/descent.ML"
 use "Tools/Function/scnp_solve.ML"
 use "Tools/Function/scnp_reconstruct.ML"