1.1 --- a/src/Pure/Isar/proof.ML	Thu Jan 08 12:15:23 2009 +0100
     1.2 +++ b/src/Pure/Isar/proof.ML	Thu Jan 08 13:18:34 2009 +0100
     1.3 @@ -345,7 +345,8 @@
     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, before_qed, after_qed}))) =
     1.8 +    fun prt_goal (SOME (ctxt, (i,
     1.9 +      {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
    1.10            pretty_facts "using " ctxt
    1.11              (if mode <> Backward orelse null using then NONE else SOME using) @
    1.12            [Pretty.str ("goal" ^