diff -r f16c9e6401d1 -r 28f1181c1a48 src/Pure/Isar/proof.ML
--- 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" ^