--- a/src/HOL/Hyperreal/NSA.thy Thu May 17 19:49:21 2007 +0200
+++ b/src/HOL/Hyperreal/NSA.thy Thu May 17 19:49:40 2007 +0200
@@ -671,13 +671,13 @@
0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
fun reorient_proc sg _ (_ $ t $ u) =
case u of
- Const("HOL.zero", _) => NONE
- | Const("HOL.one", _) => NONE
- | Const("Numeral.number_of", _) $ _ => NONE
+ Const(@{const_name HOL.zero}, _) => NONE
+ | Const(@{const_name HOL.one}, _) => NONE
+ | Const(@{const_name Numeral.number_of}, _) $ _ => NONE
| _ => SOME (case t of
- Const("HOL.zero", _) => meta_zero_approx_reorient
- | Const("HOL.one", _) => meta_one_approx_reorient
- | Const("Numeral.number_of", _) $ _ =>
+ Const(@{const_name HOL.zero}, _) => meta_zero_approx_reorient
+ | Const(@{const_name HOL.one}, _) => meta_one_approx_reorient
+ | Const(@{const_name Numeral.number_of}, _) $ _ =>
meta_number_of_approx_reorient);
in