src/Pure/Thy/thy_output.ML

           make_span (the cmd) (toks1 @ (tok2 :: (toks3 @ the_default [] tok4))));
 
     val spans = toks
       |> take_suffix Token.is_space |> #1
       |> Source.of_list
-      |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token)) NONE
-      |> Source.source stopper (Scan.error (Scan.bulk span)) NONE
+      |> Source.source' 0 Token.stopper (Scan.error (Scan.bulk token))
+      |> Source.source stopper (Scan.error (Scan.bulk span))
       |> Source.exhaust;
 
 
     (* present commands *)