| changeset 66452 | 450cefec7c11 |
| parent 65460 | fe4cf0de13cb |
| child 67621 | 8f93d878f855 |
--- a/src/Pure/context.ML Thu Aug 17 22:29:30 2017 +0200 +++ b/src/Pure/context.ML Fri Aug 18 13:55:05 2017 +0200 @@ -165,9 +165,7 @@ val finished = ~1; fun display_name thy_id = - let - val {name = long_name, stage} = history_of_id thy_id; - val name = Long_Name.base_name long_name; + let val {name, stage} = history_of_id thy_id; in if stage = finished then name else name ^ ":" ^ string_of_int stage end; fun display_names thy =