src/HOL/Divides.thy
changeset 38715 6513ea67d95d
parent 37767 a2b7a20d6ea3
child 39489 8bb7f32a3a08
     1.1 --- a/src/HOL/Divides.thy	Wed Aug 25 18:19:04 2010 +0200
     1.2 +++ b/src/HOL/Divides.thy	Wed Aug 25 18:36:22 2010 +0200
     1.3 @@ -700,7 +700,7 @@
     1.4  
     1.5  in
     1.6  
     1.7 -val cancel_div_mod_nat_proc = Simplifier.simproc @{theory}
     1.8 +val cancel_div_mod_nat_proc = Simplifier.simproc_global @{theory}
     1.9    "cancel_div_mod" ["(m::nat) + n"] (K CancelDivMod.proc);
    1.10  
    1.11  val _ = Addsimprocs [cancel_div_mod_nat_proc];
    1.12 @@ -1459,7 +1459,7 @@
    1.13  
    1.14  in
    1.15  
    1.16 -val cancel_div_mod_int_proc = Simplifier.simproc @{theory}
    1.17 +val cancel_div_mod_int_proc = Simplifier.simproc_global @{theory}
    1.18    "cancel_zdiv_zmod" ["(k::int) + l"] (K CancelDivMod.proc);
    1.19  
    1.20  val _ = Addsimprocs [cancel_div_mod_int_proc];