| changeset 50201 | c26369c9eda6 |
| parent 48866 | 034df7b05759 |
| child 52106 | 090a519982e9 |
| 50200:2c94c065564e | 50201:c26369c9eda6 |
|---|---|
153 |
153 |
154 (* print *) |
154 (* print *) |
155 |
155 |
156 fun pretty path = |
156 fun pretty path = |
157 let val s = implode_path path |
157 let val s = implode_path path |
158 in Pretty.mark (Isabelle_Markup.path s) (Pretty.str (quote s)) end; |
158 in Pretty.mark (Markup.path s) (Pretty.str (quote s)) end; |
159 |
159 |
160 val print = Pretty.str_of o pretty; |
160 val print = Pretty.str_of o pretty; |
161 |
161 |
162 |
162 |
163 (* base element *) |
163 (* base element *) |