diff -r 1e341728bae9 -r 97921d23ebe3 src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Sat Feb 01 20:46:19 2014 +0100
+++ b/src/HOL/SAT.thy	Sat Feb 01 21:09:53 2014 +0100
@@ -13,14 +13,12 @@
 
 ML_file "Tools/prop_logic.ML"
 ML_file "Tools/sat_solver.ML"
-ML_file "Tools/sat_funcs.ML"
+ML_file "Tools/sat.ML"
 
-ML {* structure sat = SATFunc(cnf) *}
-
-method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o sat.sat_tac) *}
+method_setup sat = {* Scan.succeed (SIMPLE_METHOD' o SAT.sat_tac) *}
   "SAT solver"
 
-method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o sat.satx_tac) *}
+method_setup satx = {* Scan.succeed (SIMPLE_METHOD' o SAT.satx_tac) *}
   "SAT solver (with definitional CNF)"
 
 end