equal
deleted
inserted
replaced
212 raw_size_thms = raw_size_thms} |
212 raw_size_thms = raw_size_thms} |
213 in |
213 in |
214 (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_result, lthy1) |
214 (raw_bclauses, raw_bn_funs, raw_bn_eqs, raw_result, lthy1) |
215 end |
215 end |
216 *} |
216 *} |
217 |
|
218 ML {* |
|
219 infix 1 ||>>> |>>> |
|
220 |
|
221 fun (x |>>> f) = |
|
222 let |
|
223 val (x', y') = f x |
|
224 in |
|
225 ([x'], y') |
|
226 end |
|
227 |
|
228 fun (([], y) ||>>> f) = ([], y) |
|
229 | ((xs, y) ||>>> f) = |
|
230 let |
|
231 val (x', y') = f y |
|
232 in |
|
233 (xs @ [x'], y') |
|
234 end; |
|
235 (op ||>>) |
|
236 *} |
|
237 |
|
238 |
217 |
239 |
218 |
240 ML {* |
219 ML {* |
241 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = |
220 fun nominal_datatype2 opt_thms_name dts bn_funs bn_eqs bclauses lthy = |
242 let |
221 let |