equal
deleted
inserted
replaced
241 | _ => raise ERROR ("no type variables") |
241 | _ => raise ERROR ("no type variables") |
242 ) |
242 ) |
243 end |
243 end |
244 *} |
244 *} |
245 |
245 |
|
246 |
246 text {* produces the definition for a lifted constant *} |
247 text {* produces the definition for a lifted constant *} |
247 |
248 |
248 ML {* |
249 ML {* |
249 fun get_const_def nconst oconst rty qty lthy = |
250 fun get_const_def nconst oconst rty qty lthy = |
250 let |
251 let |
256 |> map Free |
257 |> map Free |
257 |
258 |
258 val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys |
259 val rep_fns = map (fst o get_fun repF rty qty lthy) arg_tys |
259 val abs_fn = (fst o get_fun absF rty qty lthy) res_ty |
260 val abs_fn = (fst o get_fun absF rty qty lthy) res_ty |
260 |
261 |
|
262 fun mk_fun_map (t1,t2) = Const (@{const_name "fun_map"}, dummyT) $ t1 $ t2 |
|
263 |
|
264 val fns = Library.foldr (mk_fun_map) (rep_fns, abs_fn) |
|
265 |> Syntax.check_term lthy |
261 in |
266 in |
262 map (op $) (rep_fns ~~ fresh_args) |
267 fns $ oconst |
263 |> curry list_comb oconst |
|
264 |> curry (op $) abs_fn |
|
265 |> fold_rev lambda fresh_args |
|
266 end |
268 end |
267 *} |
269 *} |
268 |
270 |
269 ML {* |
271 ML {* |
270 fun exchange_ty rty qty ty = |
272 fun exchange_ty rty qty ty = |