--- a/src/HOL/SAT.thy Fri Mar 13 19:53:09 2009 +0100
+++ b/src/HOL/SAT.thy Fri Mar 13 19:58:26 2009 +0100
@@ -28,10 +28,10 @@
ML {* structure sat = SATFunc(structure cnf = cnf); *}
-method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}
+method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *}
"SAT solver"
-method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *}
+method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *}
"SAT solver (with definitional CNF)"
end