anchor.diff:              begin
               match (SS.compress a).n with
               | Tm_name x ->
  -            if name_exists_in x ctx
  -            ||  name_exists_in x pat_binders
  -            then //we already have x
  -                    //so don't include it in the quasi-pattern
  -                    aux (S.mk_binder formal :: pat_binders) formals t_res args
  -            else let x = {x with sort=formal.sort} in
  -                    let subst = [NT(formal, S.bv_to_name x)] in
  -                    let formals = SS.subst_binders subst formals in
  -                    let t_res = SS.subst subst t_res in
  -                    aux (S.mk_binder ({x with sort=formal.sort}) :: pat_binders) formals t_res args
  +                if name_exists_in x ctx
  +                ||  name_exists_in x pat_binders
  +                then //we already have x
  +                        //so don't include it in the quasi-pattern
  +                        aux (S.mk_binder formal :: pat_binders) formals t_res args
  +                else let x = {x with sort=formal.sort} in
  +                        let subst = [NT(formal, S.bv_to_name x)] in
  +                        let formals = SS.subst_binders subst formals in
  +                        let t_res = SS.subst subst t_res in
  +                        aux (S.mk_binder ({x with sort=formal.sort}) :: pat_binders) formals t_res args
               | _ -> //it's not a name, so it can't be included in the patterns
               aux (S.mk_binder formal :: pat_binders) formals t_res args
               end
  
positive.code:               aux (bs@[y, imp]) (bs_terms@[S.bv_to_name y, imp]) formals wl
           in
           aux [] [] formals wl
      in
  
      let imitate_app (orig:prob) (env:Env.env) (wl:worklist)
  
negative.code:           if is_app rhs
            then imitate_app orig env wl lhs bs_lhs t_res_lhs rhs
            else if is_arrow rhs
            then imitate_arrow orig env wl lhs bs_lhs t_res_lhs EQ rhs
            else giveup_or_defer env orig wl
                                 (BU.format1 "first_order heursitic cannot solve %s; \
                                              rhs not an app or arrow"
  