equal
deleted
inserted
replaced
63 case bmode of |
63 case bmode of |
64 Lst => (mk_append, bind_lst) |
64 Lst => (mk_append, bind_lst) |
65 | Set => (mk_union, bind_set) |
65 | Set => (mk_union, bind_set) |
66 | Res => (mk_union, bind_set) |
66 | Res => (mk_union, bind_set) |
67 in |
67 in |
68 foldl1 combine_fn (map (bind_fn lthy args) bodies) |
68 bodies |
|
69 |> map (bind_fn lthy args) |
|
70 |> foldl1 combine_fn |
69 end |
71 end |
70 |
72 |
71 (* produces the term for an alpha with abstraction *) |
73 (* produces the term for an alpha with abstraction *) |
72 fun mk_alpha_term bmode fv alpha args args' binders binders' = |
74 fun mk_alpha_term bmode fv alpha args args' binders binders' = |
73 let |
75 let |