--- a/src/HOL/Real/real_arith.ML Fri Jul 11 09:02:27 2008 +0200
+++ b/src/HOL/Real/real_arith.ML Fri Jul 11 09:02:28 2008 +0200
@@ -36,7 +36,7 @@
lessD = lessD, (*Can't change lessD: the reals are dense!*)
neqE = neqE,
simpset = simpset addsimps simps}) #>
- arith_inj_const ("RealDef.real", HOLogic.natT --> HOLogic.realT) #>
- arith_inj_const ("RealDef.real", HOLogic.intT --> HOLogic.realT)
+ arith_inj_const (@{const_name real}, HOLogic.natT --> HOLogic.realT) #>
+ arith_inj_const (@{const_name real}, HOLogic.intT --> HOLogic.realT)
end;