| changeset 32187 | cca43ca13f4f |
| parent 32145 | 220c9e439d39 |
| child 32197 | bc341bbe4417 |
--- a/src/Pure/goal.ML Sat Jul 25 00:53:47 2009 +0200 +++ b/src/Pure/goal.ML Sat Jul 25 10:31:27 2009 +0200 @@ -78,7 +78,7 @@ (case Thm.nprems_of th of 0 => conclude th | n => raise THM ("Proof failed.\n" ^ - Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals_without_context n th)) ^ + Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context n th)) ^ ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));