equal
deleted
inserted
replaced
62 in |
62 in |
63 Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2 |
63 Const (@{const_name "prod_alpha"}, [ty1, ty2] ---> resT) $ t1 $ t2 |
64 end |
64 end |
65 |
65 |
66 (* generates the compound binder terms *) |
66 (* generates the compound binder terms *) |
67 fun mk_binders lthy bmode args bodies = |
67 fun mk_binders lthy bmode args binders = |
68 let |
68 let |
69 fun bind_set lthy args (NONE, i) = setify lthy (nth args i) |
69 fun bind_set lthy args (NONE, i) = setify lthy (nth args i) |
70 | bind_set _ args (SOME bn, i) = bn $ (nth args i) |
70 | bind_set _ args (SOME bn, i) = bn $ (nth args i) |
71 fun bind_lst lthy args (NONE, i) = listify lthy (nth args i) |
71 fun bind_lst lthy args (NONE, i) = listify lthy (nth args i) |
72 | bind_lst _ args (SOME bn, i) = bn $ (nth args i) |
72 | bind_lst _ args (SOME bn, i) = bn $ (nth args i) |
75 case bmode of |
75 case bmode of |
76 Lst => (mk_append, bind_lst) |
76 Lst => (mk_append, bind_lst) |
77 | Set => (mk_union, bind_set) |
77 | Set => (mk_union, bind_set) |
78 | Res => (mk_union, bind_set) |
78 | Res => (mk_union, bind_set) |
79 in |
79 in |
80 bodies |
80 binders |
81 |> map (bind_fn lthy args) |
81 |> map (bind_fn lthy args) |
82 |> foldl1 combine_fn |
82 |> foldl1 combine_fn |
83 end |
83 end |
84 |
84 |
85 (* produces the term for an alpha with abstraction *) |
85 (* produces the term for an alpha with abstraction *) |