anchor.diff:    | Some (Meta _) -> true
     | _ -> false
   
  +and p_binder is_atomic b =
  +  let b', t', catf = p_binder' is_atomic b in
  +  match t' with
  +  | Some typ -> catf b' typ
  +  | None -> b'
  +
   (* is_atomic is true if the binder must be parsed atomically *)
  -and p_binder' (is_atomic: bool) (b: binder): document * option<document> * (document -> document -> document) =
  +and p_binder' (is_atomic: bool) (b: binder): document * option<document> * catf =
     match b.b with
     | Variable lid -> optional p_aqual b.aqual ^^ p_lident lid, None, cat_with_colon
     | TVariable lid -> p_lident lid, None, cat_with_colon
  
positive.code: // is to be printed in. For more details see the `annotation_style` type
  // definition.
  and p_tmArrow style p_Tm e =
    let terms = p_tmArrow' p_Tm e in
    let terms', last = List.splitAt (List.length terms - 1) terms in
    let n, last_n, terms', sep, last_op =
      match style with
  
negative.code:         else p_appTerm t, None, cat_with_colon (* This choice seems valid (used in p_tmNoEq') *)
      end
  
  and p_refinement aqual_opt binder t phi =
    let b, typ = p_refinement' aqual_opt binder t phi in
    cat_with_colon b typ
  
  and p_refinement' aqual_opt binder t phi =
    let is_t_atomic =
  