# HG changeset patch
# User wenzelm
# Date 1189149092 -7200
# Node ID ec228ae5a620a5ae30d7a8c1fa02420055913701
# Parent  c8cee92b06bc2ccc8dcfb7c21caffa4e0be3e987
made smlnj happy;

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