src/HOL/IntDiv.thy
changeset 32010 cb1a1c94b4cd
parent 31998 2c7a24f74db9
child 32075 e8e0fb5da77a
     1.1 --- a/src/HOL/IntDiv.thy	Wed Jul 15 23:11:57 2009 +0200
     1.2 +++ b/src/HOL/IntDiv.thy	Wed Jul 15 23:48:21 2009 +0200
     1.3 @@ -266,7 +266,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val cancel_div_mod_int_proc = Simplifier.simproc (the_context ())
     1.8 +val cancel_div_mod_int_proc = Simplifier.simproc @{theory}
     1.9    "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
    1.10  
    1.11  val _ = Addsimprocs [cancel_div_mod_int_proc];