diff -r c4728771f04f -r 3ec2d35b380f src/HOL/SAT.thy
--- a/src/HOL/SAT.thy	Fri Mar 13 19:18:07 2009 +0100
+++ b/src/HOL/SAT.thy	Fri Mar 13 23:56:07 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