src/HOL/int_arith1.ML
changeset 24196 f1dbfd7e3223
parent 24093 5d0ecd0c8f3c
child 24266 bdb48fd8fbdd
     1.1 --- a/src/HOL/int_arith1.ML	Thu Aug 09 15:52:45 2007 +0200
     1.2 +++ b/src/HOL/int_arith1.ML	Thu Aug 09 15:52:47 2007 +0200
     1.3 @@ -600,7 +600,7 @@
     1.4      simpset = simpset addsimps add_rules
     1.5                        addsimprocs Int_Numeral_Base_Simprocs
     1.6                        addcongs [if_weak_cong]}) #>
     1.7 -  arith_inj_const ("Nat.of_nat", HOLogic.natT --> HOLogic.intT) #>
     1.8 +  arith_inj_const (@{const_name of_nat}, HOLogic.natT --> HOLogic.intT) #>
     1.9    arith_discrete "IntDef.int"
    1.10  
    1.11  end;