equal
deleted
inserted
replaced
62 (* over all variables listed in vs (these variables *) |
62 (* over all variables listed in vs (these variables *) |
63 (* correspond to the type variables in rty) *) |
63 (* correspond to the type variables in rty) *) |
64 (* *) |
64 (* *) |
65 (* for example for: ?'a list *) |
65 (* for example for: ?'a list *) |
66 (* it produces: %a. map a *) |
66 (* it produces: %a. map a *) |
67 (* |
|
68 fun mk_mapfun ctxt vs ty = |
67 fun mk_mapfun ctxt vs ty = |
69 let |
68 let |
70 val vs' = map (mk_Free) vs |
69 val vs' = map (mk_Free) vs |
71 |
70 |
72 fun mk_mapfun_aux ty = |
71 fun mk_mapfun_aux ty = |