src/HOL/Tools/semiring_normalizer.ML
changeset 46497 89ccf66aa73d
parent 44064 5bce8ff0d9ae
child 47108 2a1953f0d20d
     1.1 --- a/src/HOL/Tools/semiring_normalizer.ML	Wed Feb 15 22:44:31 2012 +0100
     1.2 +++ b/src/HOL/Tools/semiring_normalizer.ML	Wed Feb 15 23:19:30 2012 +0100
     1.3 @@ -199,8 +199,8 @@
     1.4      fun mk_const phi cT x =
     1.5        let val (a, b) = Rat.quotient_of_rat x
     1.6        in if b = 1 then Numeral.mk_cnumber cT a
     1.7 -        else Thm.capply
     1.8 -             (Thm.capply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
     1.9 +        else Thm.apply
    1.10 +             (Thm.apply (Drule.cterm_rule (instantiate' [SOME cT] []) @{cpat "op /"})
    1.11                           (Numeral.mk_cnumber cT a))
    1.12               (Numeral.mk_cnumber cT b)
    1.13        end
    1.14 @@ -725,7 +725,7 @@
    1.15  (* Power of polynomial (optimized for the monomial and trivial cases).       *)
    1.16  
    1.17  fun num_conv n =
    1.18 -  nat_add_conv (Thm.capply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
    1.19 +  nat_add_conv (Thm.apply @{cterm Suc} (Numeral.mk_cnumber @{ctyp nat} (dest_numeral n - 1)))
    1.20    |> Thm.symmetric;
    1.21  
    1.22