equal
deleted
inserted
replaced
163 |
163 |
164 val PureN = "Pure"; |
164 val PureN = "Pure"; |
165 val finished = ~1; |
165 val finished = ~1; |
166 |
166 |
167 fun display_name thy_id = |
167 fun display_name thy_id = |
168 let |
168 let val {name, stage} = history_of_id thy_id; |
169 val {name = long_name, stage} = history_of_id thy_id; |
|
170 val name = Long_Name.base_name long_name; |
|
171 in if stage = finished then name else name ^ ":" ^ string_of_int stage end; |
169 in if stage = finished then name else name ^ ":" ^ string_of_int stage end; |
172 |
170 |
173 fun display_names thy = |
171 fun display_names thy = |
174 let |
172 let |
175 val name = display_name (theory_id thy); |
173 val name = display_name (theory_id thy); |