# HG changeset patch
# User wenzelm
# Date 1474490664 -7200
# Node ID 397b25cee74c524626ccbda767f2d5c9d4d32ad4
# Parent  e149e3e320a3626483c1944cf3ba6d0a45a00538
\<^raw> output is intended for LaTeX;

diff -r e149e3e320a3 -r 397b25cee74c src/Pure/Thy/html.ML
--- 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;