src/HOL/Decision_Procs/Commutative_Ring.thy

   then show ?thesis by (simp only: norm_ci)
 qed
 
 
 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