src/HOL/SAT.thy

--- a/src/HOL/SAT.thy	Wed Oct 31 11:23:21 2012 +0100
+++ b/src/HOL/SAT.thy	Wed Oct 31 11:23:21 2012 +0100
@@ -8,7 +8,7 @@
 header {* Reconstructing external resolution proofs for propositional logic *}
 
 theory SAT
-imports Refute
+imports Hilbert_Choice List Sledgehammer
 begin
 
 ML_file "Tools/sat_funcs.ML"