src/HOL/Library/Eval.thy
changeset 26591 74b3c93f2428
parent 26587 58fb6e033c00
child 27103 d8549f4d900b
equal deleted inserted replaced
26590:9114b5fe533a 26591:74b3c93f2428
   182 parse_translation {*
   182 parse_translation {*
   183 let
   183 let
   184   fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
   184   fun rterm_of_tr [t] = Lexicon.const @{const_name rterm_of} $ t
   185     | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
   185     | rterm_of_tr ts = raise TERM ("rterm_of_tr", ts);
   186 in
   186 in
   187   [("\<^fixed>rterm_of_syntax", rterm_of_tr)]
   187   [(Syntax.fixedN ^ "rterm_of_syntax", rterm_of_tr)]
   188 end
   188 end
   189 *}
   189 *}
   190 
   190 
   191 setup {*
   191 setup {*
   192 let
   192 let