-type attrs = E.node_attrs
-
-type bind = Void (* *)
- | Abst of N.level * term (* level, type *)
- | Abbr of term (* body *)
-
-and term = Sort of attrs * int (* attrs, hierarchy index *)
- | LRef of attrs * int (* attrs, position index *)
- | GRef of attrs * uri (* attrs, reference *)
- | Cast of attrs * term * term (* attrs, type, term *)
- | Appl of attrs * term * term (* attrs, argument, function *)
- | Bind of attrs * bind * term (* attrs, binder, scope *)
+type n_attrs = E.node_attrs
+type a_attrs = E.appl_attrs
+type b_attrs = E.bind_attrs
+
+(* x-reduced abstractions are output by RTM only *)
+type bind = Void (* *)
+ | Abst of bool * N.layer * term (* x-reduced?, layer, type *)
+ | Abbr of term (* body *)
+
+and term = Sort of int (* hierarchy index *)
+ | LRef of n_attrs * int (* attrs, position index *)
+ | GRef of n_attrs * uri (* attrs, reference *)
+ | Cast of term * term (* type, term *)
+ | Appl of a_attrs * term * term (* attrs, argument, function *)
+ | Bind of b_attrs * bind * term (* attrs, binder, scope *)