src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Wed Jul 15 23:11:57 2009 +0200
+++ b/src/HOL/Divides.thy	Wed Jul 15 23:48:21 2009 +0200
@@ -655,7 +655,7 @@
 
 in
 
-val cancel_div_mod_nat_proc = Simplifier.simproc (the_context ())
+val cancel_div_mod_nat_proc = Simplifier.simproc @{theory}
   "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
 
 val _ = Addsimprocs [cancel_div_mod_nat_proc];