src/Pure/Thy/thy_output.ML
changeset 70067 0cb8753bdb50
parent 70064 f8293bf510a0
child 70068 b9985133805d
     1.1 --- a/src/Pure/Thy/thy_output.ML	Sat Mar 09 13:35:49 2019 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Sat Mar 09 23:57:07 2019 +0100
     1.3 @@ -449,7 +449,7 @@
     1.4    in
     1.5      if length command_results = length spans then
     1.6        ((NONE, []), NONE, true, [], (I, I))
     1.7 -      |> present (Toplevel.init ()) (spans ~~ command_results)
     1.8 +      |> present (Toplevel.init_toplevel ()) (spans ~~ command_results)
     1.9        |> present_trailer
    1.10        |> rev
    1.11      else error "Messed-up outer syntax for presentation"