anchor.diff:          group (concat [
                       lbrace; (doc_of_term e); space; str "with"; space;
                       separate_map space 
  -                        (fun ((l:FStar.Ident.lid),e) -> str l.str ^^ equals ^^ doc_of_term e)
  +                        (fun (l,e) -> concat [str l.str; equals; doc_of_term e])
                           fields;
                       rbrace])
     | Record(None, fields) ->
           group (concat [
                       lbrace; 
                       separate_map space
  -                        (fun ((l:FStar.Ident.lid),e) -> (str l.str) ^^ equals ^^ (doc_of_term e))
  +                        (fun (l,e) -> concat [(str l.str); equals; (doc_of_term e)])
                           fields;
                       rbrace
                       ])
     | Project(e,l) ->
  -        group (doc_of_term e ^^ dot ^^ str l.str)
  +        group (concat [doc_of_term e; dot; str l.str])
     | Product([], t) ->
           group (doc_of_term t)
     | Product(b::hd::tl, t) ->
  
positive.code:                  (separate_map hardline 
                       (fun (p,w,e) -> concat [(str " | ");
                                               (doc_of_pat p); space; 
                                               (match w with | None -> empty | Some e -> str "when " ^^ (doc_of_term e));
                                               space; (str "->"); space;
                                               (doc_of_term e)])
                       branches)])
  
negative.code:     | _ -> empty 
  
  let doc_of_const x = match x with
    | Const_effect -> str "eff"
    | Const_unit -> str "()"
    | Const_bool b -> str (if b then "true" else "false")
    | Const_float x ->  str (Util.string_of_float x)
    | Const_char x ->   squotes (document_of_char x )
    | Const_string(bytes, _) -> dquotes (str (Util.string_of_bytes bytes))
    | Const_bytearray _  ->  str "<bytearray>"
    | Const_int (x, _) -> str x
    | Const_range r -> str (Range.string_of_range r)
    | Const_reify
    | Const_reflect _ -> str "unsupported constant"
  
  // SI: maybe do nesting for terms with args? 
  let rec doc_of_term (x:term) = match x.tm with
  