--- 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))