diff -r 55ef4d0bc250 -r e070a6ab1891 src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jul 07 00:15:02 2007 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Sat Jul 07 00:15:02 2007 +0200
@@ -37,14 +37,14 @@
 fun xsymbols_output s =
   if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
     let val syms = Symbol.explode s
-    in (implode (map xsym_output syms), real (Symbol.length syms)) end
-  else Symbol.default_output s;
+    in (implode (map xsym_output syms), Symbol.length syms) end
+  else Output.default_output s;
 
 in
 
 fun setup_xsymbols_output () =
-  Output.add_mode Symbol.xsymbolsN
-    (xsymbols_output, K xsymbols_output, Symbol.default_indent, Symbol.encode_raw);
+  (Output.add_mode Symbol.xsymbolsN xsymbols_output Symbol.encode_raw;
+   Pretty.add_mode Symbol.xsymbolsN Pretty.default_indent Pretty.default_markup);
 
 end;
 
@@ -65,7 +65,7 @@
 fun xml_atom kind x = XML.element "atom" [("kind", kind)] [XML.text x];
 
 fun tagit (kind, bg_tag) x =
-  (bg_tag () ^ x ^ end_tag (), real (Symbol.length (Symbol.explode x)));
+  (bg_tag () ^ x ^ end_tag (), Symbol.length (Symbol.explode x));
 
 fun free_or_skolem x =
   (case try Name.dest_skolem x of