--- a/src/Pure/display.ML Fri Dec 12 22:13:13 2008 +0100
+++ b/src/Pure/display.ML Sat Dec 13 15:00:39 2008 +0100
@@ -213,7 +213,7 @@
||> List.partition (Defs.plain_args o #2 o #1);
val rests = restricts |> map (apfst (apfst extern_const)) |> sort_wrt (#1 o #1);
in
- [Pretty.strs ("names:" :: Context.names_of thy)] @
+ [Pretty.strs ("names:" :: Context.display_names thy)] @
[Pretty.strs ["name prefix:", NameSpace.path_of naming],
Pretty.big_list "classes:" (map pretty_classrel clsses),
pretty_default default,
--- 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