diff -r c0844a30ea4e -r a7897aebbffc src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Tue Jan 09 15:29:17 2001 +0100
+++ b/src/HOL/Hyperreal/Star.thy	Tue Jan 09 15:32:27 2001 +0100
@@ -25,11 +25,11 @@
                         ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
     
     starfun :: (real => real) => hypreal => hypreal        ("*f* _" [80] 80)
-    "*f* f  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel```{%n. f(X n)}))" 
+    "*f* f  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel``{%n. f(X n)}))" 
 
     (* internal functions *)
     starfun_n :: (nat => (real => real)) => hypreal => hypreal        ("*fn* _" [80] 80)
-    "*fn* F  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel```{%n. (F n)(X n)}))" 
+    "*fn* F  == (%x. Abs_hypreal(UN X: Rep_hypreal(x). hyprel``{%n. (F n)(X n)}))" 
 
     InternalFuns :: (hypreal => hypreal) set
     "InternalFuns == {X. EX F. X = *fn* F}"