author | wenzelm |
Wed, 21 Sep 2016 22:44:24 +0200 | |
changeset 63934 | 397b25cee74c |
parent 63933 | e149e3e320a3 |
child 63935 | aa1fe1103ab8 |
--- a/src/Pure/Thy/html.ML Wed Sep 21 22:43:06 2016 +0200 +++ b/src/Pure/Thy/html.ML Wed Sep 21 22:44:24 2016 +0200 @@ -48,11 +48,9 @@ val no_symbols = make_symbols []; fun output_sym (Symbols tab) s = - if Symbol.is_raw s then Symbol.decode_raw s - else - (case Symtab.lookup tab s of - SOME x => x - | NONE => XML.text s); + (case Symtab.lookup tab s of + SOME x => x + | NONE => XML.text s); end;