diff -r 9114b5fe533a -r 74b3c93f2428 src/HOL/Library/Eval.thy
--- a/src/HOL/Library/Eval.thy	Wed Apr 09 20:46:44 2008 +0200
+++ b/src/HOL/Library/Eval.thy	Wed Apr 09 20:47:17 2008 +0200
@@ -184,7 +184,7 @@
   fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
     | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
 in
-  [("\<^fixed>rterm_of_syntax", rterm_of_tr)]
+  [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)]
 end
 *}