+ let map1 (lenv, a, wws) (id, w) =
+ let attr = name_of_id id in
+ let ww = xlate_term C.start st lenv w in
+ D.push2 C.err C.start lenv attr ~t:ww (), attr :: a, ww :: wws
+ in
+ let map2 (lenv, a, n) id =
+ let attr = name_of_id id in
+ D.push2 C.err C.start lenv attr (), attr :: a, succ n
+ in
+ let lenv, aa, bb = match b with