src/HOL/Algebra/abstract/Ring2.thy

   in
     val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc);
   end;
 *}
 
-ML_setup {* Addsimprocs [ring_simproc] *}
+ML {* Addsimprocs [ring_simproc] *}
 
 lemma natsum_ldistr:
   "!!a::'a::ring. setsum f {..n::nat} * a = setsum (%i. f i * a) {..n}"
 by (induct n) simp_all