anchor.diff:      | _ -> p_tmImplies e
   
   and p_tmImplies e = match e.tm with
  -    | Op({idText = "==>"}, [e1;e2]) -> infix0 (str "==>") (p_tmArrow p_tmFormula e1) (p_tmImplies e2)
  -    | _ -> p_tmArrow p_tmFormula e
  +    | Op({idText = "==>"}, [e1;e2]) -> infix0 (str "==>") (p_tmArrow (Arrows (2, 2)) p_tmFormula e1) (p_tmImplies e2)
  +    | _ -> p_tmArrow (Arrows (2, 2)) p_tmFormula e
   
   (* This function is somewhat convoluted because it is used in a few different contexts and it's trying to properly  *)
   (* indent for each of them. For signatures, it is trying to print the whole arrow on one line. If this fails, it    *)
   (* tries to print everything except the last term on the same line and push the last term on a new line. If this    *)
   (* fails, it prints every term on a separate line. This seems consistent with the current style used in most cases. *)
   (* A trailing space may sometimes be introduced, which we should trim.                                              *)
  -and p_tmArrow p_Tm e =
  +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 last_op = if List.length terms > 1 then space ^^ rarrow else empty in
  +  let n, last_n, terms', sep, last_op =
  +    match style with
  +    | Arrows (n, ln)-> n, ln, terms', space ^^ rarrow ^^ break1, rarrow ^^ space
  +    | Binders (n, ln) -> n, ln, List.map soft_parens_with_nesting terms', break1, colon ^^ space
  +  in
  +  let last_op = if List.length terms > 1 then last_op else empty in
  +  let single_line_arg_indent = repeat n space in
     match List.length terms with
     | 1 -> List.hd terms
  -  | _ -> group (ifflat (separate (space ^^ rarrow ^^ break1) terms)
  -             (prefix2 (group ((ifflat ((separate (space ^^ rarrow ^^ break1) terms') ^^ last_op)
  -                  (jump2 ((separate (space ^^ rarrow ^^ break1) terms') ^^ last_op))))) (List.hd last)))
  +  | _ -> 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 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:             (p_trigger trigger))) term_doc)
    | _ -> p_simpleTerm ps pb e
  
  and p_quantifier e = match e.tm with
      | QForall _ -> str "forall"
      | QExists _ -> str "exists"
  
negative.code:           has_attrs = false;
            is_fsdoc = false })
    | Val(lid, t) ->
      // str "val" ^^ space ^^ p_lident lid ^^ group (colon ^^ space ^^ alt_p_typ false false t) //(p_typ false false t))
      group (str "val" ^^ space ^^ p_lident lid ^^ space ^^ (alt_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 =
  