more uniform output (cf. 450cefec7c11);
authorwenzelm
Tue May 15 17:07:41 2018 +0200 (12 months ago)
changeset 6819273a1b393d6f9
parent 68189 6163c90694ef
child 68193 14dd78f036ba
more uniform output (cf. 450cefec7c11);
src/Pure/context.ML
     1.1 --- a/src/Pure/context.ML	Tue May 15 13:57:39 2018 +0200
     1.2 +++ b/src/Pure/context.ML	Tue May 15 17:07:41 2018 +0200
     1.3 @@ -177,7 +177,7 @@
     1.4  fun display_names thy =
     1.5    let
     1.6      val name = display_name (theory_id thy);
     1.7 -    val ancestor_names = map theory_name (ancestors_of thy);
     1.8 +    val ancestor_names = map theory_long_name (ancestors_of thy);
     1.9    in rev (name :: ancestor_names) end;
    1.10  
    1.11  val pretty_thy = Pretty.str_list "{" "}" o display_names;