src/HOL/IntDiv.thy

     in ArithData.prove_conv all_tac (ArithData.simp_all_tac simps) end;
 end)
 
 in
 
-val cancel_zdiv_zmod_proc = Simplifier.simproc @{theory}
+val cancel_zdiv_zmod_proc = Simplifier.simproc (the_context ())
   "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
 
 end;
 
 Addsimprocs [cancel_zdiv_zmod_proc]