src/HOL/Tools/semiring_normalizer.ML

      | t => Rat.rat_of_int (snd (HOLogic.dest_number t))) 
        handle TERM _ => error "ring_dest_const")
     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
   in funs key
      {is_const = K numeral_is_const,

  end;
 
 (* 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;
 
 
 val polynomial_pow_conv =
  let