src/HOL/Tools/nat_numeral_simprocs.ML
changeset 38864 4abe644fcea5
parent 37388 793618618f78
child 40878 7695e4de4d86
     1.1 --- a/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/nat_numeral_simprocs.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -168,7 +168,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 =" HOLogic.natT
     1.8 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
     1.9    val bal_add1 = @{thm nat_eq_add_iff1} RS trans
    1.10    val bal_add2 = @{thm nat_eq_add_iff2} RS trans
    1.11  );
    1.12 @@ -300,7 +300,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 =" HOLogic.natT
    1.17 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
    1.18    val cancel = @{thm nat_mult_eq_cancel1} RS trans
    1.19    val neg_exchanges = false
    1.20  )
    1.21 @@ -380,7 +380,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 =" HOLogic.natT
    1.26 +  val dest_bal = HOLogic.dest_bin @{const_name HOL.eq} HOLogic.natT
    1.27    fun simp_conv _ _ = SOME @{thm nat_mult_eq_cancel_disj}
    1.28  );
    1.29