--- a/src/HOL/SAT.thy Mon Mar 16 17:51:24 2009 +0100
+++ b/src/HOL/SAT.thy Mon Mar 16 18:24:30 2009 +0100
@@ -1,5 +1,4 @@
(* Title: HOL/SAT.thy
- ID: $Id$
Author: Alwen Tiu, Tjark Weber
Copyright 2005
@@ -28,10 +27,10 @@
ML {* structure sat = SATFunc(structure cnf = cnf); *}
-method_setup sat = {* Method.no_args (SIMPLE_METHOD' sat.sat_tac) *}
+method_setup sat = {* Scan.succeed (K (SIMPLE_METHOD' sat.sat_tac)) *}
"SAT solver"
-method_setup satx = {* Method.no_args (SIMPLE_METHOD' sat.satx_tac) *}
+method_setup satx = {* Scan.succeed (K (SIMPLE_METHOD' sat.satx_tac)) *}
"SAT solver (with definitional CNF)"
end