src/HOL/Decision_Procs/Commutative_Ring.thy

--- a/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Apr 12 11:34:50 2012 +0200
+++ b/src/HOL/Decision_Procs/Commutative_Ring.thy	Thu Apr 12 18:39:19 2012 +0200
@@ -314,6 +314,9 @@
 
 
 use "commutative_ring_tac.ML"
-setup Commutative_Ring_Tac.setup
+
+method_setup comm_ring = {*
+  Scan.succeed (SIMPLE_METHOD' o Commutative_Ring_Tac.tac)
+*} "reflective decision procedure for equalities over commutative rings"
 
 end