src/HOL/Tools/groebner.ML
changeset 37388 793618618f78
parent 36752 cf558aeb35b0
child 37744 3daaf23b9ab4
--- a/src/HOL/Tools/groebner.ML	Tue Jun 08 16:37:19 2010 +0200
+++ b/src/HOL/Tools/groebner.ML	Tue Jun 08 16:37:22 2010 +0200
@@ -698,7 +698,7 @@
 
 val holify_polynomial =
  let fun holify_varpow (v,n) =
-  if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n)  (* FIXME *)
+  if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp nat} n)  (* FIXME *)
  fun holify_monomial vars (c,m) =
   let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
    in end_itlist ring_mk_mul (mk_const c :: xps)