--- a/src/HOL/Tools/numeral_simprocs.ML Sat Aug 28 20:24:40 2010 +0800
+++ b/src/HOL/Tools/numeral_simprocs.ML Sat Aug 28 16:14:32 2010 +0200
@@ -222,7 +222,7 @@
(open CancelNumeralsCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
val bal_add1 = @{thm eq_add_iff1} RS trans
val bal_add2 = @{thm eq_add_iff2} RS trans
);
@@ -401,7 +401,7 @@
(open CancelNumeralFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
val cancel = @{thm mult_cancel_left} RS trans
val neg_exchanges = false
)
@@ -516,7 +516,7 @@
(open CancelFactorCommon
val prove_conv = Arith_Data.prove_conv
val mk_bal = HOLogic.mk_eq
- val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
+ val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
fun simp_conv _ _ = SOME @{thm mult_cancel_left}
);
@@ -606,7 +606,7 @@
local
val zr = @{cpat "0"}
val zT = ctyp_of_term zr
- val geq = @{cpat "op ="}
+ val geq = @{cpat HOL.eq}
val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
@@ -676,7 +676,7 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name "op ="},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
+ | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
let
val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
val _ = map is_number [a,b,c]
@@ -697,7 +697,7 @@
val T = ctyp_of_term c
val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
in SOME (mk_meta_eq th) end
- | Const(@{const_name "op ="},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
+ | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
let
val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
val _ = map is_number [a,b,c]