- let f w t = f (B.Bind (id, B.Abst w, t)) in
- let f w = xlate_term (f w) t in
- xlate_term f w
+ let f w =
+ let a = [B.Name (true, id)] in
+ let f t = f (B.Bind (a, B.Abst w, t)) in
+ let f c = xlate_term c f t in
+ B.push f c a (B.Abst w)
+ in
+ xlate_term c f w
+
+let xlate_pars f pars =
+ let map f (id, w) c =
+ let a = [B.Name (true, id)] in
+ let f w = B.push f c a (B.Abst w) in
+ xlate_term c f w
+ in
+ C.list_fold_right f map pars B.empty_context