# HG changeset patch # User haftmann # Date 1215759748 -7200 # Node ID 7165068bb61fdbb7623add1f8141982768f3ed93 # Parent 5b293a8cf4762b878d1b9d0d75fe6a709dc76529 antiquotation diff -r 5b293a8cf476 -r 7165068bb61f src/HOL/Real/real_arith.ML --- 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;