# HG changeset patch
# User wenzelm
# Date 1231417114 -3600
# Node ID 438c39fc93c8f4850abb93f116b1a8d12d9c13b2
# Parent  6b258cc0134c2ecbf79c84e6d6ee0984e6dc67a8
tuned;

diff -r 6b258cc0134c -r 438c39fc93c8 src/Pure/Isar/proof.ML
--- 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" ^