src/Pure/Thy/document_output.ML
changeset 76415 f362975e8ba1
parent 76410 687fb18e805c
child 76432 d0079b509d99
--- a/src/Pure/Thy/document_output.ML	Thu Nov 03 16:08:28 2022 +0100
+++ b/src/Pure/Thy/document_output.ML	Thu Nov 03 20:10:35 2022 +0100
@@ -476,7 +476,7 @@
   in
     if length command_results = length spans then
       (([], []), NONE, true, [], (I, I))
-      |> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
+      |> present (Toplevel.make_state NONE) (spans ~~ command_results)
       |> present_trailer
       |> rev
     else error "Messed-up outer syntax for presentation"