--- a/src/HOL/arith_data.ML Wed Jun 13 03:28:21 2007 +0200
+++ b/src/HOL/arith_data.ML Wed Jun 13 03:31:11 2007 +0200
@@ -601,7 +601,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 ("IntDef.int", HOLogic.natT --> HOLogic.intT) $ n)
+ (Const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) $ n)
val t1_lt_zero = Const (@{const_name Orderings.less},
HOLogic.intT --> HOLogic.intT --> HOLogic.boolT) $ t1 $ zero_int
val not_false = HOLogic.mk_Trueprop (HOLogic.Not $ HOLogic.false_const)