--- a/src/Pure/Isar/proof.ML Tue Nov 21 20:48:11 2006 +0100
+++ b/src/Pure/Isar/proof.ML Tue Nov 21 20:58:15 2006 +0100
@@ -331,7 +331,7 @@
(case filter_out (equal "") strs of [] => ""
| strs' => enclose " (" ")" (commas strs'));
- fun prt_goal (SOME (ctxt, (i, {using, goal, before_qed, after_qed, ...}))) =
+ fun prt_goal (SOME (ctxt, (i, {statement = _, using, goal, before_qed, after_qed}))) =
pretty_facts "using " ctxt
(if mode <> Backward orelse null using then NONE else SOME using) @
[Pretty.str ("goal" ^