# HG changeset patch
# User haftmann
# Date 1231398371 -3600
# Node ID bc41c9cbbfc2b3c935e6ca168c115217cb59e4d7
# Parent  4638ab6c878f80507cbe61028b67680b60f97726
made SML/NJ happy

diff -r 4638ab6c878f -r bc41c9cbbfc2 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Wed Jan 07 22:33:04 2009 +0100
+++ b/src/Pure/Isar/proof.ML	Thu Jan 08 08:06:11 2009 +0100
@@ -345,7 +345,7 @@
       (case filter_out (fn s => s = "") strs of [] => ""
       | strs' => enclose " (" ")" (commas strs'));
 
-    fun prt_goal (SOME (ctxt, (i, {statement = ((_, pos), _, _), messages, using, goal, ...}))) =
+    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" ^