src/Pure/Isar/toplevel.ML
changeset 60245 79ad597fe699
parent 60190 906de96ba68a
child 60403 9be917b2f376
     1.1 --- a/src/Pure/Isar/toplevel.ML	Sun May 03 17:41:54 2015 +0200
     1.2 +++ b/src/Pure/Isar/toplevel.ML	Sun May 03 17:52:27 2015 +0200
     1.3 @@ -382,9 +382,9 @@
     1.4            val lthy = f thy;
     1.5            val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy);
     1.6            val _ =
     1.7 -            if begin then
     1.8 -              Output.state (Pretty.string_of (Pretty.chunks (Local_Theory.pretty lthy)))
     1.9 -            else ();
    1.10 +            (case Local_Theory.pretty lthy of
    1.11 +              [] => ()
    1.12 +            | prts => Output.state (Pretty.string_of (Pretty.chunks prts)));
    1.13          in Theory (gthy, SOME lthy) end
    1.14      | _ => raise UNDEF));
    1.15