src/HOL/SAT.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 32232 6c394343360f
--- 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