-and exp_bind e a b out tab =
- let f a ns = a, ns in
- let a, ns = Y.get_names f a in
- match b with
- | D.Abst (n, ws) ->
- let e = D.push_bind C.start e a (D.Abst (n, [])) in
- let attrs = [XL.level n; XL.name ns; XL.mark a; XL.arity ws] in
- XL.tag XL.abst attrs ~contents:(list_rev_iter exp_term e ns ws) out tab
- | D.Abbr vs ->
- let e = D.push_bind C.start e a (D.Abbr []) in
- let attrs = [XL.name ns; XL.mark a; XL.arity vs] in
- XL.tag XL.abbr attrs ~contents:(list_rev_iter exp_term e ns vs) out tab
- | D.Void n ->
- let attrs = [XL.name a; XL.mark a; XL.arity ~n []] in
- XL.tag XL.void attrs out tab
+and exp_bind st e a y b out tab = match b with
+ | D.Abst (_, n, w) ->
+ let attrs = XL.layer st n :: XL.name y :: XL.side y @ XL.main y in
+ XL.tag XL.abst attrs ~contents:(exp_term st e w) out tab
+ | D.Abbr v ->
+ let attrs = [XL.name y] in
+ XL.tag XL.abbr attrs ~contents:(exp_term st e v) out tab
+ | D.Void ->
+ let attrs = [XL.name y] in
+ XL.tag XL.void attrs out tab