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