diff -r c8cee92b06bc -r ec228ae5a620 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Sep 06 18:19:00 2007 +0200 +++ b/src/Pure/Isar/proof.ML Fri Sep 07 09:11:32 2007 +0200 @@ -339,7 +339,8 @@ (case filter_out (equal "") strs of [] => "" | strs' => enclose " (" ")" (commas strs')); - fun prt_goal (SOME (ctxt, (i, {messages, using, goal, before_qed, after_qed, ...}))) = + fun prt_goal (SOME (ctxt, (i, + {statement = _, messages, using, goal, before_qed, after_qed}))) = pretty_facts "using " ctxt (if mode <> Backward orelse null using then NONE else SOME using) @ [Pretty.str ("goal" ^