changeset 24630 | 351a308ab58d |
parent 23261 | 85f27f79232f |
child 24996 | ebd5f4cc7118 |
--- a/src/HOL/Library/comm_ring.ML Tue Sep 18 11:06:22 2007 +0200 +++ b/src/HOL/Library/comm_ring.ML Tue Sep 18 16:08:00 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 (Integer.int i) + else pol_Pinj T $ HOLogic.mk_nat i $ (pol_PX T $ (pol_Pc T $ cring_one T) $ one $ (pol_Pc T $ cring_zero T)) end