--- a/src/HOL/Tools/semiring_normalizer.ML Wed Feb 15 22:44:31 2012 +0100
+++ b/src/HOL/Tools/semiring_normalizer.ML Wed Feb 15 23:19:30 2012 +0100
@@ -199,8 +199,8 @@
fun mk_const phi cT x =
let val (a, b) = Rat.quotient_of_rat x
in if b = 1 then Numeral.mk_cnumber cT a
- else Thm.capply
- (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
+ else Thm.apply
+ (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
(Numeral.mk_cnumber cT a))
(Numeral.mk_cnumber cT b)
end
@@ -725,7 +725,7 @@
(* Power of polynomial (optimized for the monomial and trivial cases). *)
fun num_conv n =
- nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
+ nat_add_conv (Thm.apply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
|> Thm.symmetric;