equal
deleted
inserted
replaced
282 |
282 |
283 fun get_fun_fun fs_tys = |
283 fun get_fun_fun fs_tys = |
284 let |
284 let |
285 val (fs, tys) = split_list fs_tys |
285 val (fs, tys) = split_list fs_tys |
286 val ([oty1, oty2], [nty1, nty2]) = split_list tys |
286 val ([oty1, oty2], [nty1, nty2]) = split_list tys |
287 val oty = Type ("fun", [nty1, oty2]) |
287 val oty = nty1 --> oty2 |
288 val nty = Type ("fun", [oty1, nty2]) |
288 val nty = oty1 --> nty2 |
289 val ftys = map (op -->) tys |
289 val ftys = map (op -->) tys |
290 in |
290 in |
291 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
291 (list_comb (Const (@{const_name "fun_map"}, ftys ---> oty --> nty), fs), (oty, nty)) |
292 end |
292 end |
293 |
293 |