--- 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" ^