--- a/src/HOL/Tools/lin_arith.ML Thu Aug 09 15:52:45 2007 +0200
+++ b/src/HOL/Tools/lin_arith.ML Thu Aug 09 15:52:47 2007 +0200
@@ -478,7 +478,7 @@
val terms2 = map (subst_term [(split_term, zero_nat)]) rev_terms
val t1' = incr_boundvars 1 t1
val t1_eq_int_n = Const ("op =", HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1' $
- (Const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) $ n)
+ (Const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) $ n)
val t1_lt_zero = Const (@{const_name HOL.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)