src/HOL/int_arith1.ML

--- a/src/HOL/int_arith1.ML	Thu Aug 09 15:52:45 2007 +0200
+++ b/src/HOL/int_arith1.ML	Thu Aug 09 15:52:47 2007 +0200
@@ -600,7 +600,7 @@
     simpset = simpset addsimps add_rules
                       addsimprocs Int_Numeral_Base_Simprocs
                       addcongs [if_weak_cong]}) #>
-  arith_inj_const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) #>
+  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
   arith_discrete "IntDef.int"
 
 end;