| changeset 28262 | aa7ca36d67fd |
| parent 27667 | 62500b980749 |
| child 28562 | 4e74209f113e |
--- a/src/HOL/IntDiv.thy Wed Sep 17 21:27:03 2008 +0200 +++ b/src/HOL/IntDiv.thy Wed Sep 17 21:27:08 2008 +0200 @@ -279,7 +279,7 @@ 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;