anchor.diff:    | _ -> group (ifflat ((separate sep terms') ^^ space ^^ last_op ^^ List.hd last)
                (prefix n 1 (group ((ifflat (separate sep terms')
                     (jump2 ((single_line_arg_indent ^^ separate (sep ^^ single_line_arg_indent) (List.map (fun x -> align (hang 2 x)) terms'))))))) (align (hang last_n (last_op ^^ List.hd last)))))
  +
  +and all_binders_annot e =
  +  let rec all_binders e l =
  +    match e.tm with
  +    | Product(bs, tgt) -> if List.for_all is_binder_annot bs then all_binders tgt (l+ List.length bs) else (false, 0)
  +    | _ -> (true, l+1)
  +  in
  +  let b, l = all_binders e 0 in
  +  if b && l > 1 then true else false
   
   and p_tmArrow' p_Tm e = match e.tm with
     | Product(bs, tgt) -> (List.map (fun b -> p_binder false b) bs) @ (p_tmArrow' p_Tm tgt)
  
positive.code: and is_meta_qualifier aq =
    match aq with
    | Some (Meta _) -> true
    | _ -> false
  
  (* is_atomic is true if the binder must be parsed atomically *)
  
negative.code:           has_attrs = false;
            is_fsdoc = false })
    | Val(lid, t) ->
      if all_binders_annot t then
        group (str "val" ^^ space ^^ p_lident lid ^^ space ^^ (alt_p_typ (Binders (4,0)) false false t))
      else
        group (str "val" ^^ space ^^ p_lident lid ^^ group (colon ^^ space ^^ alt_p_typ (Arrows (2,2)) false false t))
      // str "val" ^^ space ^^ p_lident lid ^^ group (colon ^^ space ^^ alt_p_typ false false t) //(p_typ false false t))
  
      (* KM : not exactly sure which one of the cases below and above is used for 'assume val ..'*)
    | Assume(id, t) ->
      let decl_keyword =
  