src/Pure/Interface/proof_general.ML

   if not (exists_string (equal "\\") s) then (s, real (size s))
   else
     let val syms = Symbol.explode s
     in (implode (map (fn "\\" => "\\\\" | c => c) syms), real (Symbol.length syms)) end;
 
-fun setup_xsymbols_output () = Symbol.add_mode "xsymbols" xsymbols_output;
+fun setup_xsymbols_output () = Symbol.add_mode "xsymbols" (xsymbols_output, Symbol.default_indent);
 
 
 (* messages *)
 
 val plain_output = Library.std_output o suffix "\n";

 end;
 
 
 end;
 
-(*this hack avoids problems with escapes in ML commands; required for
-  Proof General 3.2*)
+(*a hack for Proof General 3.2 to avoid problems with escapes in ML commands*)
 infix \\\\ val op \\\\ = op \\;