author | wenzelm |
Tue, 15 May 2018 17:07:41 +0200 | |
changeset 68192 | 73a1b393d6f9 |
parent 68189 | 6163c90694ef |
child 68193 | 14dd78f036ba |
--- 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;