src/Pure/goal.ML
changeset 49847 ed5080c03165
parent 49845 9b19c0e81166
child 49893 0d4106850eb2
     1.1 --- a/src/Pure/goal.ML	Sat Oct 13 18:04:11 2012 +0200
     1.2 +++ b/src/Pure/goal.ML	Sat Oct 13 19:53:04 2012 +0200
     1.3 @@ -87,12 +87,7 @@
     1.4    (case Thm.nprems_of th of
     1.5      0 => th
     1.6    | n => raise THM ("Proof failed.\n" ^
     1.7 -      Pretty.string_of (Pretty.chunks
     1.8 -        (Goal_Display.pretty_goals
     1.9 -          (ctxt
    1.10 -            |> Config.put Goal_Display.goals_limit n
    1.11 -            |> Config.put Goal_Display.show_main_goal true) th)) ^
    1.12 -      "\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th]));
    1.13 +      Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]));
    1.14  
    1.15  fun finish ctxt = check_finished ctxt #> conclude;
    1.16