anchor.diff:        //before inspecting any syntactic form that has binding structure
         //you must call SS.open_* to replace de Bruijn indexes with names
         let xs, body = SS.open_term xs body in
  -      let xs = if (Options.print_implicits()) then xs else filter_imp xs in
  +      let xs = if Options.print_implicits () then xs else filter_imp xs in
  +      let body_bv = FStar.Syntax.Free.names body in
         let patterns = xs |> List.choose (fun (x, qual) ->
           //x.sort contains a type annotation for the bound variable
           //the pattern `p` below only contains the variable, not the annotation
           //but, if the user wrote the annotation, then we should record that and print it back
           //additionally, if we're in verbose mode, e.g., if --print_bound_var_types is set
           //    then we should print the annotation too
  -        resugar_bv_as_pat x qual)
  +        resugar_bv_as_pat x qual body_bv)
         in
         let body = resugar_term body in
         mk (A.Abs(patterns, body))
  
positive.code:       // When resugaring it will be just a normal (explicitly bound) variable.
        begin match string_to_op v.ppname.idText with
         | Some (op, _) -> mk (A.PatOp (Ident.mk_ident (op, v.ppname.idRange)))
         | None ->
           let var_used_in_branch = Util.set_mem v branch_bv in
           mk (if not var_used_in_branch then A.PatWild
               else A.PatVar (bv_as_unique_ident v, to_arg_qual imp_opt))
        end
  
      | Pat_wild _ -> mk (A.PatWild)
  
      | Pat_dot_term (bv, term) ->
        (* TODO : this should never be resugared unless in a comment *)
        let pat = mk (A.PatVar(bv_as_unique_ident bv, Some A.Implicit)) in
        if Options.print_bound_var_types() then
          mk (A.PatAscribed(pat, resugar_term term))
        else
          pat
    in
    aux p None
  
  
negative.code:         A.mk_binder (A.Annotated (bv_as_unique_ident x, e)) r A.Type_level imp
    end
  
  and resugar_bv_as_pat' (v: S.bv) aqual (body_bv: BU.set<bv>) typ_opt =
    let mk a = A.mk_pattern a (S.range_of_bv v) in
    let used = BU.set_mem v body_bv in
    let pat =
      mk (if used
          then A.PatVar (bv_as_unique_ident v, aqual)
          else A.PatWild) in // FIXME aqual on ``_``
    match typ_opt with
    | None | Some { n = Tm_unknown } -> pat
    | Some typ -> if Options.print_bound_var_types ()
                 then mk (A.PatAscribed (pat, resugar_term typ))
                 else pat
  
  and resugar_bv_as_pat (x:S.bv) qual body_bv: option<A.pattern> =
    BU.map_opt (resugar_arg_qual qual)
      (fun aqual -> resugar_bv_as_pat' x aqual body_bv (Some <| SS.compress x.sort))
  
  and resugar_pat (p:S.pat) (branch_bv: set<bv>) : A.pattern =
    (* We lose information when desugar PatAscribed to able to resugar it back *)
  