src/HOL/IntDiv.thy
changeset 28262 aa7ca36d67fd
parent 27667 62500b980749
child 28562 4e74209f113e
     1.1 --- a/src/HOL/IntDiv.thy	Wed Sep 17 21:27:03 2008 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Sep 17 21:27:08 2008 +0200
     1.3 @@ -279,7 +279,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val cancel_zdiv_zmod_proc = Simplifier.simproc @{theory}
     1.8 +val cancel_zdiv_zmod_proc = Simplifier.simproc (the_context ())
     1.9    "cancel_zdiv_zmod" ["(m::int) + n"] (K CancelDivMod.proc)
    1.10  
    1.11  end;