diff -r 27f1b5cc5f9b -r c879d88d038a src/Pure/ProofGeneral/proof_general_emacs.ML
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 26 17:24:15 2008 +0200
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML	Fri Sep 26 19:07:56 2008 +0200
@@ -41,7 +41,7 @@
   | xsym_output s = if Symbol.is_raw s then Symbol.decode_raw s else s;
 
 fun xsymbols_output s =
-  if print_mode_active Symbol.xsymbolsN andalso exists_string (equal "\\") s then
+  if print_mode_active Symbol.xsymbolsN andalso exists_string (fn c => c = "\\") s then
     let val syms = Symbol.explode s
     in (implode (map xsym_output syms), Symbol.length syms) end
   else Output.default_output s;