src/HOL/Divides.thy

--- a/src/HOL/Divides.thy	Wed Sep 17 21:27:03 2008 +0200
+++ b/src/HOL/Divides.thy	Wed Sep 17 21:27:08 2008 +0200
@@ -371,7 +371,7 @@
 
 structure CancelDivMod = CancelDivModFun(CancelDivModData);
 
-val cancel_div_mod_proc = Simplifier.simproc @{theory}
+val cancel_div_mod_proc = Simplifier.simproc (the_context ())
   "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
 
 Addsimprocs[cancel_div_mod_proc];