# HG changeset patch
# User wenzelm
# Date 1526396861 -7200
# Node ID 73a1b393d6f90dd537119976e08c0ed0a67ecbce
# Parent  6163c90694efaf3676469286747a3383cd83f718
more uniform output (cf. 450cefec7c11);

diff -r 6163c90694ef -r 73a1b393d6f9 src/Pure/context.ML
--- a/src/Pure/context.ML	Tue May 15 13:57:39 2018 +0200
+++ b/src/Pure/context.ML	Tue May 15 17:07:41 2018 +0200
@@ -177,7 +177,7 @@
 fun display_names thy =
   let
     val name = display_name (theory_id thy);
-    val ancestor_names = map theory_name (ancestors_of thy);
+    val ancestor_names = map theory_long_name (ancestors_of thy);
   in rev (name :: ancestor_names) end;
 
 val pretty_thy = Pretty.str_list "{" "}" o display_names;