1.1 --- a/src/Pure/Isar/outer_lex.ML	Thu Aug 28 00:33:09 2008 +0200
     1.2 +++ b/src/Pure/Isar/outer_lex.ML	Thu Aug 28 00:33:11 2008 +0200
     1.3 @@ -200,7 +200,7 @@
     1.4    | AltString => x |> enclose "`" "`" o escape "`"
     1.5    | Verbatim => x |> enclose "{*" "*}"
     1.6    | Comment => x |> enclose "(*" "*)"
     1.7 -  | Malformed => Output.escape (translate_string Output.output x)
     1.8 +  | Malformed => space_implode " " (explode x)
     1.9    | Sync => ""
    1.10    | EOF => ""
    1.11    | _ => x);