src/HOL/Tools/groebner.ML
changeset 37388 793618618f78
parent 36752 cf558aeb35b0
child 37744 3daaf23b9ab4
equal deleted inserted replaced
37387:3581483cca6c 37388:793618618f78
   696  in (vars,map (grobify_equation vars) cjs)
   696  in (vars,map (grobify_equation vars) cjs)
   697  end;
   697  end;
   698 
   698 
   699 val holify_polynomial =
   699 val holify_polynomial =
   700  let fun holify_varpow (v,n) =
   700  let fun holify_varpow (v,n) =
   701   if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp "nat"} n)  (* FIXME *)
   701   if n = 1 then v else ring_mk_pow v (Numeral.mk_cnumber @{ctyp nat} n)  (* FIXME *)
   702  fun holify_monomial vars (c,m) =
   702  fun holify_monomial vars (c,m) =
   703   let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
   703   let val xps = map holify_varpow (filter (fn (_,n) => n <> 0) (vars ~~ m))
   704    in end_itlist ring_mk_mul (mk_const c :: xps)
   704    in end_itlist ring_mk_mul (mk_const c :: xps)
   705   end
   705   end
   706  fun holify_polynomial vars p =
   706  fun holify_polynomial vars p =