--- a/src/Pure/Thy/thy_output.ML Thu Apr 16 13:48:10 2015 +0200
+++ b/src/Pure/Thy/thy_output.ML Thu Apr 16 14:18:32 2015 +0200
@@ -614,16 +614,12 @@
local
-fun proof_state state =
- (case try (Proof.goal o Toplevel.proof_of) state of
- SOME {goal, ...} => goal
- | _ => error "No proof state");
-
fun goal_state name main = antiquotation name (Scan.succeed ())
(fn {state, context = ctxt, ...} => fn () =>
output ctxt
[Goal_Display.pretty_goal
- (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
+ (Config.put Goal_Display.show_main_goal main ctxt)
+ (#goal (Proof.goal (Toplevel.proof_of state)))]);
in