src/HOL/Integ/IntDiv_setup.ML
changeset 14387 e96d5c42c4b0
parent 13517 42efec18f5b2
child 14479 0eca4aabf371
     1.1 --- a/src/HOL/Integ/IntDiv_setup.ML	Sat Feb 14 02:06:12 2004 +0100
     1.2 +++ b/src/HOL/Integ/IntDiv_setup.ML	Sun Feb 15 10:46:37 2004 +0100
     1.3 @@ -13,7 +13,7 @@
     1.4  val div_name = "Divides.op div";
     1.5  val mod_name = "Divides.op mod";
     1.6  val mk_binop = HOLogic.mk_binop;
     1.7 -val mk_sum = Int_Numeral_Simprocs.mk_sum;
     1.8 +val mk_sum = Int_Numeral_Simprocs.mk_sum HOLogic.intT;
     1.9  val dest_sum = Int_Numeral_Simprocs.dest_sum;
    1.10  
    1.11  (*logic*)