--- 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"