src/Pure/goal.ML

--- a/src/Pure/goal.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/goal.ML	Mon Jul 20 21:20:09 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.pretty_goals n th)) ^
+      Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals n th)) ^
       ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th]));