src/HOL/FunDef.thy

--- a/src/HOL/FunDef.thy	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/FunDef.thy	Wed Oct 31 11:23:21 2012 +0100
@@ -5,13 +5,10 @@
 header {* Function Definitions and Termination Proofs *}
 
 theory FunDef
-imports Partial_Function Wellfounded
+imports Partial_Function SAT Wellfounded
 keywords "function" "termination" :: thy_goal and "fun" :: thy_decl
 begin
 
-ML_file "Tools/prop_logic.ML"
-ML_file "Tools/sat_solver.ML"
-
 subsection {* Definitions with default value. *}
 
 definition