src/HOL/SAT.thy

--- a/src/HOL/SAT.thy	Thu Sep 29 20:54:45 2016 +0200
+++ b/src/HOL/SAT.thy	Thu Sep 29 20:54:45 2016 +0200
@@ -8,12 +8,13 @@
 section \<open>Reconstructing external resolution proofs for propositional logic\<close>
 
 theory SAT
-imports HOL
+imports Argo
 begin
 
 ML_file "Tools/prop_logic.ML"
 ML_file "Tools/sat_solver.ML"
 ML_file "Tools/sat.ML"
+ML_file "Tools/Argo/argo_sat_solver.ML"
 
 method_setup sat = \<open>Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac)\<close>
   "SAT solver"