--- a/src/HOL/SAT.thy Sat Oct 08 23:43:15 2005 +0200
+++ b/src/HOL/SAT.thy Sun Oct 09 17:06:03 2005 +0200
@@ -30,10 +30,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 (Method.SIMPLE_METHOD (sat.sat_tac 1)) *}
"SAT solver"
-method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD sat.satx_tac) *}
+method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *}
"SAT solver (with definitional CNF)"
end