diff -r fe539d517750 -r b55a273ede18 src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun Jun 19 14:36:06 2011 +0200
+++ b/src/Pure/Thy/html.scala	Sun Jun 19 15:22:58 2011 +0200
@@ -86,7 +86,6 @@
             else if (symbols.is_bold_decoded(s1)) {
               add(hidden(s1)); add(span("bold", List(XML.Text(s2()))))
             }
-            else if (s1 == "\\<^loc>") { add(hidden(s1)); add(span("loc", List(XML.Text(s2())))) }
             else t ++= s1
           }
           flush()