diff -r fd3c60ad9155 -r cb1a1c94b4cd src/HOL/IntDiv.thy
--- a/src/HOL/IntDiv.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/IntDiv.thy	Wed Jul 15 23:48:21 2009 +0200
@@ -266,7 +266,7 @@
 
 in
 
-val cancel_div_mod_int_proc = Simplifier.simproc (the_context ())
+val cancel_div_mod_int_proc = Simplifier.simproc @{theory}
   "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
 
 val _ = Addsimprocs [cancel_div_mod_int_proc];