equal
deleted
inserted
replaced
175 in if stage = finished then name else name ^ ":" ^ string_of_int stage end; |
175 in if stage = finished then name else name ^ ":" ^ string_of_int stage end; |
176 |
176 |
177 fun display_names thy = |
177 fun display_names thy = |
178 let |
178 let |
179 val name = display_name (theory_id thy); |
179 val name = display_name (theory_id thy); |
180 val ancestor_names = map theory_name (ancestors_of thy); |
180 val ancestor_names = map theory_long_name (ancestors_of thy); |
181 in rev (name :: ancestor_names) end; |
181 in rev (name :: ancestor_names) end; |
182 |
182 |
183 val pretty_thy = Pretty.str_list "{" "}" o display_names; |
183 val pretty_thy = Pretty.str_list "{" "}" o display_names; |
184 |
184 |
185 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy); |
185 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_polyml o pretty_thy); |