author | wenzelm |
Wed, 09 Apr 2008 20:47:17 +0200 | |
changeset 26591 | 74b3c93f2428 |
parent 26590 | 9114b5fe533a |
child 26592 | 44cc22b19330 |
--- 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 *}