src/Pure/Thy/thy_output.ML

 and output_comment_document ctxt (comment, syms) =
   (case comment of
     SOME kind => output_comment ctxt (kind, syms)
   | NONE => [Latex.symbols syms])
 and output_document_text ctxt syms =
-  (case Comment.read_body syms of
-    SOME res => maps (output_comment_document ctxt) res
-  | NONE => [Latex.symbols syms])
+  Comment.read_body syms |> maps (output_comment_document ctxt)
 and output_document ctxt {markdown} source =
   let
     val pos = Input.pos_of source;
     val syms = Input.source_explode source;
 

   | (SOME comment, _) => output_comment ctxt (comment, syms));
 
 in
 
 fun output_body ctxt antiq bg en syms =
-  (case Comment.read_body syms of
-    SOME res => maps (output_comment_symbols ctxt {antiq = antiq}) res
-  | NONE => output_symbols syms) |> Latex.enclose_body bg en
+  Comment.read_body syms
+  |> maps (output_comment_symbols ctxt {antiq = antiq})
+  |> Latex.enclose_body bg en
 and output_token ctxt tok =
   let
     fun output antiq bg en =
       output_body ctxt antiq bg en (Input.source_explode (Token.input_of tok));
   in

 
 fun output_source ctxt s =
   output_body ctxt false "" "" (Symbol_Pos.explode (s, Position.none));
 
 fun check_comments ctxt =
-  Comment.read_body #> (Option.app o List.app) (fn (comment, syms) =>
+  Comment.read_body #> List.app (fn (comment, syms) =>
     let
       val pos = #1 (Symbol_Pos.range syms);
       val _ =
         comment |> Option.app (fn kind =>
           Context_Position.reports ctxt (map (pair pos) (Markup.cartouche :: Comment.markups kind)));