170 prt_typ_no_tvars T, Pretty.str " ::", Pretty.brk 1, prt_sort S]; |
170 prt_typ_no_tvars T, Pretty.str " ::", Pretty.brk 1, prt_sort S]; |
171 |
171 |
172 val tfrees = map (fn v => TFree (v, [])); |
172 val tfrees = map (fn v => TFree (v, [])); |
173 fun pretty_type syn (t, (Type.LogicalType n, _)) = |
173 fun pretty_type syn (t, (Type.LogicalType n, _)) = |
174 if syn then NONE |
174 if syn then NONE |
175 else SOME (prt_typ (Type (t, tfrees (Name.invent_list [] "'a" n)))) |
175 else SOME (prt_typ (Type (t, tfrees (Name.invents Name.context Name.aT n)))) |
176 | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) = |
176 | pretty_type syn (t, (Type.Abbreviation (vs, U, syn'), _)) = |
177 if syn <> syn' then NONE |
177 if syn <> syn' then NONE |
178 else SOME (Pretty.block |
178 else SOME (Pretty.block |
179 [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U]) |
179 [prt_typ (Type (t, tfrees vs)), Pretty.str " =", Pretty.brk 1, prt_typ U]) |
180 | pretty_type syn (t, (Type.Nonterminal, _)) = |
180 | pretty_type syn (t, (Type.Nonterminal, _)) = |