--- a/src/Pure/Isar/proof.ML Thu Jan 08 12:15:23 2009 +0100
+++ b/src/Pure/Isar/proof.ML Thu Jan 08 13:18:34 2009 +0100
@@ -345,7 +345,8 @@
(case filter_out (fn s => s = "") strs of [] => ""
| strs' => enclose " (" ")" (commas strs'));
- fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, before_qed, after_qed}))) =
+ fun prt_goal (SOME (ctxt, (i,
+ {statement = ((_, pos), _, _), 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" ^