fixed IntInf ambiguity
authorhaftmann
Mon May 14 12:52:54 2007 +0200 (2007-05-14)
changeset 22963509b1da3cee1
parent 22962 4bb05ba38939
child 22964 2284e0d02e7f
fixed IntInf ambiguity
src/HOL/Library/comm_ring.ML
     1.1 --- a/src/HOL/Library/comm_ring.ML	Mon May 14 09:33:18 2007 +0200
     1.2 +++ b/src/HOL/Library/comm_ring.ML	Mon May 14 12:52:54 2007 +0200
     1.3 @@ -46,7 +46,7 @@
     1.4        in if i = 0
     1.5          then pol_PX T $ (pol_Pc T $ cring_one T)
     1.6            $ one $ (pol_Pc T $ cring_zero T)
     1.7 -        else pol_Pinj T $ HOLogic.mk_nat i
     1.8 +        else pol_Pinj T $ HOLogic.mk_nat (Intt.int i)
     1.9            $ (pol_PX T $ (pol_Pc T $ cring_one T)
    1.10              $ one $ (pol_Pc T $ cring_zero T))
    1.11          end