diff -r 2110fcd86efb -r 568a23753e3a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Mon Jul 20 20:03:19 2009 +0200
+++ b/src/Pure/Isar/proof.ML	Mon Jul 20 21:20:09 2009 +0200
@@ -318,7 +318,7 @@
 val show_main_goal = ref false;
 val verbose = ProofContext.verbose;
 
-val pretty_goals_local = Display.pretty_goals_aux o Syntax.pp;
+val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp;
 
 fun pretty_facts _ _ NONE = []
   | pretty_facts s ctxt (SOME ths) =