# HG changeset patch
# User wenzelm
# Date 1434032127 -7200
# Node ID fa9bff5cd67969e59d8fec6bf9f35aee524a38b9
# Parent  64f48e7f921f0bf47bee00e1d81f1c3cf2ada94a
made SML/NJ happy;

diff -r 64f48e7f921f -r fa9bff5cd679 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Thu Jun 11 15:44:00 2015 +0200
+++ b/src/Pure/Isar/proof.ML	Thu Jun 11 16:15:27 2015 +0200
@@ -373,7 +373,7 @@
     val {context = ctxt, facts, mode, goal = _} = top state;
     val verbose = Config.get ctxt Proof_Context.verbose;
 
-    fun prt_goal (SOME (_, (_, {using, goal, ...}))) =
+    fun prt_goal (SOME (_, (_, {statement = _, using, goal, before_qed = _, after_qed = _}))) =
           pretty_sep
             (pretty_facts ctxt "using"
               (if mode <> Backward orelse null using then NONE else SOME using))