src/Pure/Thy/thy_output.ML

     fun present _ [] = I
       | present st ((span, (tr, st')) :: rest) = present_command tr span st st' #> present st' rest;
   in
     if length command_results = length spans then
       ((NONE, []), NONE, true, [], (I, I))
-      |> present Toplevel.toplevel (spans ~~ command_results)
+      |> present (Toplevel.init ()) (spans ~~ command_results)
       |> present_trailer
       |> rev
     else error "Messed-up outer syntax for presentation"
   end;