# HG changeset patch
# User haftmann
# Date 1179139974 -7200
# Node ID 509b1da3cee18d0f021773ba34a957dd1b12f5d7
# Parent  4bb05ba389394a61e271cf26f7db5068817c3e2f
fixed IntInf ambiguity

diff -r 4bb05ba38939 -r 509b1da3cee1 src/HOL/Library/comm_ring.ML
--- 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