src/HOL/Tools/Groebner_Basis/normalizer.ML
changeset 23259 ccee01b8d1c5
parent 23252 67268bb40b21
child 23330 01c09922ce59
     1.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Jun 05 18:36:07 2007 +0200
     1.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer.ML	Tue Jun 05 18:36:09 2007 +0200
     1.3 @@ -5,8 +5,8 @@
     1.4  
     1.5  signature NORMALIZER = 
     1.6  sig
     1.7 - val mk_cnumber : ctyp -> int -> cterm
     1.8 - val mk_cnumeral : int -> cterm
     1.9 + val mk_cnumber : ctyp -> integer -> cterm
    1.10 + val mk_cnumeral : integer -> cterm
    1.11   val semiring_normalize_conv : Proof.context -> Conv.conv
    1.12   val semiring_normalize_tac : Proof.context -> int -> tactic
    1.13   val semiring_normalize_wrapper :  NormalizerData.entry -> Conv.conv
    1.14 @@ -36,9 +36,8 @@
    1.15  fun mk_cnumeral 0 = pls_const
    1.16    | mk_cnumeral ~1 = min_const
    1.17    | mk_cnumeral i =
    1.18 -      let val (q, r) = IntInf.divMod (i, 2)
    1.19 -      in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (IntInf.toInt r)) 
    1.20 -      end;
    1.21 +      let val (q, r) = Integer.divmod i 2
    1.22 +      in Thm.capply (Thm.capply bit_const (mk_cnumeral q)) (mk_cbit (Integer.machine_int r)) end;
    1.23  
    1.24  fun mk_cnumber cT = 
    1.25   let