clarified signature;

--- a/src/Pure/General/comment.ML	Sat Feb 03 20:34:26 2018 +0100
+++ b/src/Pure/General/comment.ML	Sat Feb 03 20:46:28 2018 +0100
@@ -13,7 +13,7 @@
   val scan_cancel: (kind * Symbol_Pos.T list) scanner
   val scan_latex: (kind * Symbol_Pos.T list) scanner
   val scan: (kind * Symbol_Pos.T list) scanner
-  val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list option
+  val read_body: Symbol_Pos.T list -> (kind option * Symbol_Pos.T list) list
 end;
 
 structure Comment: COMMENT =
@@ -76,9 +76,9 @@
   scan_permissive Comment || scan_permissive Cancel || scan_permissive Latex;
 
 fun read_body syms =
-  if exists (is_symbol o Symbol_Pos.symbol) syms then
+  (if exists (is_symbol o Symbol_Pos.symbol) syms then
     Scan.read Symbol_Pos.stopper (Scan.repeat scan_body) syms
-  else NONE;
+  else NONE) |> the_default [(NONE, syms)];
 
 end;
 

--- a/src/Pure/Thy/thy_output.ML	Sat Feb 03 20:34:26 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Sat Feb 03 20:46:28 2018 +0100
@@ -60,9 +60,7 @@
     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;
@@ -122,9 +120,9 @@
 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 =
@@ -148,7 +146,7 @@
   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 _ =