1.1 --- a/src/Pure/Isar/proof.ML	Wed Jan 07 22:33:04 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jan 08 08:06:11 2009 +0100
     1.3 @@ -345,7 +345,7 @@
     1.4        (case filter_out (fn s => s = "") strs of [] => ""
     1.5        | strs' => enclose " (" ")" (commas strs'));
     1.6  
     1.7 -    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, ...}))) =
     1.8 +    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
     1.9            pretty_facts "using " ctxt
    1.10              (if mode <> Backward orelse null using then NONE else SOME using) @
    1.11            [Pretty.str ("goal" ^