src/Pure/old_goals.ML

--- a/src/Pure/old_goals.ML	Fri Dec 12 22:13:13 2008 +0100
+++ b/src/Pure/old_goals.ML	Sat Dec 13 15:00:39 2008 +0100
@@ -127,7 +127,7 @@
 
 (*Generates the list of new theories when the proof state's theory changes*)
 fun thy_error (thy,thy') =
-  let val names = Context.names_of thy' \\ Context.names_of thy
+  let val names = Context.display_names thy' \\ Context.display_names thy
   in  case names of
         [name] => "\nNew theory: " ^ name
       | _       => "\nNew theories: " ^ space_implode ", " names