src/HOL/Tools/numeral_simprocs.ML
changeset 38864 4abe644fcea5
parent 38549 d0385f2764d8
child 40878 7695e4de4d86
     1.1 --- a/src/HOL/Tools/numeral_simprocs.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/numeral_simprocs.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -222,7 +222,7 @@
     1.4   (open CancelNumeralsCommon
     1.5    val prove_conv = Arith_Data.prove_conv
     1.6    val mk_bal   = HOLogic.mk_eq
     1.7 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
     1.8 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
     1.9    val bal_add1 = @{thm eq_add_iff1} RS trans
    1.10    val bal_add2 = @{thm eq_add_iff2} RS trans
    1.11  );
    1.12 @@ -401,7 +401,7 @@
    1.13   (open CancelNumeralFactorCommon
    1.14    val prove_conv = Arith_Data.prove_conv
    1.15    val mk_bal   = HOLogic.mk_eq
    1.16 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    1.17 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
    1.18    val cancel = @{thm mult_cancel_left} RS trans
    1.19    val neg_exchanges = false
    1.20  )
    1.21 @@ -516,7 +516,7 @@
    1.22   (open CancelFactorCommon
    1.23    val prove_conv = Arith_Data.prove_conv
    1.24    val mk_bal   = HOLogic.mk_eq
    1.25 -  val dest_bal = HOLogic.dest_bin "op =" Term.dummyT
    1.26 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} Term.dummyT
    1.27    fun simp_conv _ _ = SOME @{thm mult_cancel_left}
    1.28  );
    1.29  
    1.30 @@ -606,7 +606,7 @@
    1.31  local
    1.32   val zr = @{cpat "0"}
    1.33   val zT = ctyp_of_term zr
    1.34 - val geq = @{cpat "op ="}
    1.35 + val geq = @{cpat HOL.eq}
    1.36   val eqT = Thm.dest_ctyp (ctyp_of_term geq) |> hd
    1.37   val add_frac_eq = mk_meta_eq @{thm "add_frac_eq"}
    1.38   val add_frac_num = mk_meta_eq @{thm "add_frac_num"}
    1.39 @@ -676,7 +676,7 @@
    1.40          val T = ctyp_of_term c
    1.41          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "divide_le_eq"}
    1.42        in SOME (mk_meta_eq th) end
    1.43 -  | Const(@{const_name "op ="},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    1.44 +  | Const(@{const_name HOL.eq},_)$(Const(@{const_name Rings.divide},_)$_$_)$_ =>
    1.45        let
    1.46          val ((a,b),c) = Thm.dest_binop ct |>> Thm.dest_binop
    1.47          val _ = map is_number [a,b,c]
    1.48 @@ -697,7 +697,7 @@
    1.49          val T = ctyp_of_term c
    1.50          val th = instantiate' [SOME T] (map SOME [a,b,c]) @{thm "le_divide_eq"}
    1.51        in SOME (mk_meta_eq th) end
    1.52 -  | Const(@{const_name "op ="},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    1.53 +  | Const(@{const_name HOL.eq},_)$_$(Const(@{const_name Rings.divide},_)$_$_) =>
    1.54      let
    1.55        val (a,(b,c)) = Thm.dest_binop ct ||> Thm.dest_binop
    1.56          val _ = map is_number [a,b,c]