--- a/src/Pure/goal.ML Fri Sep 03 20:39:38 2010 +0200
+++ b/src/Pure/goal.ML Fri Sep 03 21:13:53 2010 +0200
@@ -83,7 +83,10 @@
0 => ()
| n => raise THM ("Proof failed.\n" ^
Pretty.string_of (Pretty.chunks
- (Goal_Display.pretty_goals ctxt {total = true, main = true, maxgoals = n} th)) ^
+ (Goal_Display.pretty_goals
+ (ctxt
+ |> Config.put Goal_Display.goals_limit n
+ |> Config.put Goal_Display.show_main_goal true) th)) ^
"\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th]));
fun finish ctxt th = (check_finished ctxt th; conclude th);