258 | print_stmt (name, Code_Thingol.Classinst |
258 | print_stmt (name, Code_Thingol.Classinst |
259 { class, tyco, vs, inst_params, superinst_params, ... }) = |
259 { class, tyco, vs, inst_params, superinst_params, ... }) = |
260 let |
260 let |
261 val tyvars = intro_tyvars vs reserved; |
261 val tyvars = intro_tyvars vs reserved; |
262 val classtyp = (class, tyco `%% map (ITyVar o fst) vs); |
262 val classtyp = (class, tyco `%% map (ITyVar o fst) vs); |
263 fun print_classparam_instance ((classparam, const as { dom, ... }), (thm, _)) = |
263 fun print_classparam_instance ((classparam, (const as { dom, ... }, _)), (thm, _)) = |
264 let |
264 let |
265 val aux_dom = Name.invent_names (snd reserved) "a" dom; |
265 val aux_dom = Name.invent_names (snd reserved) "a" dom; |
266 val auxs = map fst aux_dom; |
266 val auxs = map fst aux_dom; |
267 val vars = intro_vars auxs reserved; |
267 val vars = intro_vars auxs reserved; |
268 val aux_abstr = if null auxs then [] else [enum "," "(" ")" |
268 val aux_abstr = if null auxs then [] else [enum "," "(" ")" |