src/HOL/Divides.thy
changeset 20044 92cc2f4c7335
parent 18702 7dc7dcd63224
child 20217 25b068a99d2b
     1.1 --- a/src/HOL/Divides.thy	Sat Jul 08 12:54:29 2006 +0200
     1.2 +++ b/src/HOL/Divides.thy	Sat Jul 08 12:54:30 2006 +0200
     1.3 @@ -208,7 +208,7 @@
     1.4  structure CancelDivMod = CancelDivModFun(CancelDivModData);
     1.5  
     1.6  val cancel_div_mod_proc = NatArithUtils.prep_simproc
     1.7 -      ("cancel_div_mod", ["(m::nat) + n"], CancelDivMod.proc);
     1.8 +      ("cancel_div_mod", ["(m::nat) + n"], K CancelDivMod.proc);
     1.9  
    1.10  Addsimprocs[cancel_div_mod_proc];
    1.11  *}