src/Pure/Thy/thy_output.ML

--- a/src/Pure/Thy/thy_output.ML	Mon May 13 06:50:37 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML	Mon May 13 12:40:17 2013 +0200
@@ -612,7 +612,8 @@
 
 fun goal_state name main = antiquotation name (Scan.succeed ())
   (fn {state, context = ctxt, ...} => fn () => output ctxt
-    [Goal_Display.pretty_goal {main = main, limit = true} ctxt (proof_state state)]);
+    [Goal_Display.pretty_goal
+      (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
 
 in