anchor.diff:          (x::l), e, x
     in
   
  -  let rec aux' (top:bool) (loc:lenv_t) env (p:pattern)
  +  let rec aux (loc:lenv_t) (env:env_t) (p:pattern)
       : lenv_t                         (* list of all BVs mentioned *)
       * env_t                          (* env updated with the BVs pushed in *)
       * bnd                            (* a binder for the pattern *)
  
positive.code:         let t1, aq0 = desugar_term_aq env t1 in
          let env, binder, pat = desugar_binding_pat_maybe_top top_level env pat in
          let tm, aq1 =
              match binder with
              | LetBinder(l, (t, _tacopt)) -> //_tacopt must be None here
                let body, aq = desugar_term_aq env t2 in
                let fv = S.lid_as_fv l (incr_delta_qualifier t1) None in
                mk <| Tm_let((false, [mk_lb (attrs, Inr fv, t, t1, t1.pos)]), body), aq
  
              | LocalBinder (x,_) ->
                  // TODO GGGGG unsure if keep _ or [] on second comp below
                let body, aq = desugar_term_aq env t2 in
                let body = match pat with
                  | []
                  | [{v=Pat_wild _}, _] -> body
                  | _ ->
                    S.mk (Tm_match(S.bv_to_name x, desugar_disjunctive_pattern pat None body)) None top.range in
                mk <| Tm_let((false, [mk_lb (attrs, Inl x, x.sort, t1, t1.pos)]), Subst.close [S.mk_binder x] body), aq
          in
          tm, aq0 @ aq1
        in
  
negative.code:             | Pat_cons(fv, args) -> pos <| Pat_cons(({fv with fv_qual=Some (Record_ctor (record.typename, record.fields |> List.map fst))}), args)
              | _ -> p in
          env, e, b, p, annots
    in
  
    let aux_maybe_or env (p:pattern) =
      let loc = [] in
      match p.pat with
        | PatOr [] -> failwith "impossible"
        | PatOr (p::ps) ->
          let loc, env, var, p, ans = aux loc env p in
          let loc, env, ps = List.fold_left (fun (loc, env, ps) p ->
            let loc, env, _, p, ans = aux loc env p in
            loc, env, (p,ans)::ps) (loc, env, []) ps in
          let pats = ((p,ans)::List.rev ps) in
          env, var, pats
        | _ ->
          let loc, env, vars, pat, ans = aux loc env p in
          env, vars, [(pat, ans)]
    in
    let env, b, pats = aux_maybe_or env p in
    check_linear_pattern_variables (List.map fst pats) p.prange;
    env, b, pats
  
  and desugar_binding_pat_maybe_top top env p
    : env_t                   (* environment with patterns variables pushed in *)
    * bnd                     (* a binder for the pattern *)
    * list<annotated_pat>     (* elaborated patterns with their variable annotations *)
    =
  
    if top then
      let mklet x ty (tacopt : option<S.term>) : (env_t * bnd * list<annotated_pat>) =
      // GM: ^ I seem to need the type annotation here,
      //     or F* gets confused between tuple2 and tuple3 apparently?
          env, LetBinder(qualify env x, (ty, tacopt)), []
      in
      let op_to_ident x = mk_ident (compile_op 0 x.idText x.idRange, x.idRange) in
      match p.pat with
      | PatOp x ->
          mklet (op_to_ident x) tun None
      | PatVar (x, _) ->
  