src/HOL/Tools/nat_arith.ML
changeset 38864 4abe644fcea5
parent 38715 6513ea67d95d
child 48372 868dc809c8a2
     1.1 --- a/src/HOL/Tools/nat_arith.ML	Sat Aug 28 20:24:40 2010 +0800
     1.2 +++ b/src/HOL/Tools/nat_arith.ML	Sat Aug 28 16:14:32 2010 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4  (struct
     1.5    open CommonCancelSums;
     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 uncancel_tac = gen_uncancel_tac @{thm "nat_add_left_cancel"};
    1.10  end);
    1.11