avoid control symbols in document (\<^fixed>);
authorwenzelm
Wed, 09 Apr 2008 20:47:17 +0200
changeset 26591 74b3c93f2428
parent 26590 9114b5fe533a
child 26592 44cc22b19330
avoid control symbols in document (\<^fixed>);
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
 *}