src/HOL/Algebra/abstract/Ring2.thy

       in if t' aconv u 
         then NONE
         else SOME rew 
     end;
   in
-    val ring_simproc = Simplifier.simproc (the_context ()) "ring" lhss (K proc);
+    val ring_simproc = Simplifier.simproc @{theory} "ring" lhss (K proc);
   end;
 *}
 
 ML {* Addsimprocs [ring_simproc] *}