author | haftmann |
Mon, 14 May 2007 12:52:54 +0200 | |
changeset 22963 | 509b1da3cee1 |
parent 22962 | 4bb05ba38939 |
child 22964 | 2284e0d02e7f |
--- a/src/HOL/Library/comm_ring.ML Mon May 14 09:33:18 2007 +0200 +++ b/src/HOL/Library/comm_ring.ML Mon May 14 12:52:54 2007 +0200 @@ -46,7 +46,7 @@ in if i = 0 then pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T) - else pol_Pinj T $ HOLogic.mk_nat i + else pol_Pinj T $ HOLogic.mk_nat (Intt.int i) $ (pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)) end