--- a/src/HOL/SAT.thy Wed Nov 29 15:44:46 2006 +0100
+++ b/src/HOL/SAT.thy Wed Nov 29 15:44:51 2006 +0100
@@ -17,7 +17,7 @@
begin
text {* \medskip Late package setup: default values for refute, see
- also theory @{text Refute}. *}
+ also theory @{theory Refute}. *}
refute_params
["itself"=1,
@@ -30,10 +30,10 @@
ML {* structure sat = SATFunc(structure cnf = cnf); *}
-method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD (sat.sat_tac 1)) *}
+method_setup sat = {* Method.no_args (Method.SIMPLE_METHOD' sat.sat_tac) *}
"SAT solver"
-method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD (sat.satx_tac 1)) *}
+method_setup satx = {* Method.no_args (Method.SIMPLE_METHOD' sat.satx_tac) *}
"SAT solver (with definitional CNF)"
end