# HG changeset patch # User wenzelm # Date 1491857969 -7200 # Node ID fe4cf0de13cb030c685125d2a8d815b4dec1d9b4 # Parent da59e8e0a66316f45c39c81081809625728b58e2 proper display_name; diff -r da59e8e0a663 -r fe4cf0de13cb src/Pure/context.ML --- a/src/Pure/context.ML Mon Apr 10 21:43:21 2017 +0200 +++ b/src/Pure/context.ML Mon Apr 10 22:59:29 2017 +0200 @@ -165,7 +165,9 @@ val finished = ~1; fun display_name thy_id = - let val {name, stage} = history_of_id thy_id + let + val {name = long_name, stage} = history_of_id thy_id; + val name = Long_Name.base_name long_name; in if stage = finished then name else name ^ ":" ^ string_of_int stage end; fun display_names thy =