changeset 2163 | 5dc48e1af733 |
parent 2146 | a2f70c09e77d |
child 2213 | 231a20534950 |
child 2288 | 3b83960f9544 |
2156:029f8aabed12 | 2163:5dc48e1af733 |
---|---|
288 in |
288 in |
289 (fv_frees_exp, fv_bns_exp, simps_exp, lthy'') |
289 (fv_frees_exp, fv_bns_exp, simps_exp, lthy'') |
290 end |
290 end |
291 *} |
291 *} |
292 |
292 |
293 end |
293 (**************************************************) |
294 |
|
295 datatype foo = |
|
296 C1 nat |
|
297 | C2 foo int |
|
298 |
|
299 (* |
|
300 ML {* |
|
301 fun mk_body descr sorts fv_ty_map dtyp = |
|
302 let |
|
303 val nth_dtyp_constr_tys descr sorts |
|
304 in |
|
305 true |
|
306 end |
|
307 *} |
|
308 *) |
|
309 |
|
310 end |