anchor.diff:      in
       record
   
  +let check_linear_pattern_variables pats r =
  +  // returns the set of pattern variables
  +  let rec pat_vars p = match p.v with
  +    | Pat_dot_term _
  +    | Pat_wild _
  +    | Pat_constant _ -> S.no_names
  +    | Pat_var x -> BU.set_add x S.no_names
  +    | Pat_cons(_, pats) ->
  +      let aux out (p, _) =
  +          let intersection = BU.set_intersect (pat_vars p) out in
  +          if BU.set_is_empty intersection
  +          then BU.set_union out (pat_vars p)
  +          else
  +            let duplicate_bv = List.hd (BU.set_elements intersection) in
  +            raise_error ( Errors.Fatal_NonLinearPatternNotPermitted,
  +                          BU.format1
  +                            "Non-linear patterns are not permitted: `%s` appears more than once in this pattern."
  +                             (duplicate_bv.ppname.idText) )
  +
  +                        r
  +      in
  +      List.fold_left aux S.no_names pats
  +  in
  +
  +  // check that the same variables are bound in each pattern
  +  match pats with
  +  | [] -> ()
  +  | [p] -> pat_vars p |> ignore
  +  | p::ps ->
  +    let pvars = pat_vars p in
  +    let aux p =
  +      if BU.set_eq pvars (pat_vars p) then () else
  +      let nonlinear_vars = BU.set_symmetric_difference pvars (pat_vars p) in
  +      let first_nonlinear_var = List.hd (BU.set_elements nonlinear_vars) in
  +      raise_error ( Errors.Fatal_IncoherentPatterns,
  +                    BU.format1
  +                      "Patterns in this match are incoherent, variable %s is bound in some but not all patterns."
  +                       (first_nonlinear_var.ppname.idText) )
  +                  r
  +    in
  +    List.iter aux ps
  +
   (* TODO : Patterns should be checked that there are no incompatible type ascriptions *)
   (* and these type ascriptions should not be dropped !!!                              *)
   let rec desugar_data_pat env p : (env_t * bnd * list<annotated_pat>) =
  -  let check_linear_pattern_variables pats r =
  -    // returns the set of pattern variables
  -    let rec pat_vars p = match p.v with
  -      | Pat_dot_term _
  -      | Pat_wild _
  -      | Pat_constant _ -> S.no_names
  -      | Pat_var x -> BU.set_add x S.no_names
  -      | Pat_cons(_, pats) ->
  -        let aux out (p, _) =
  -            let intersection = BU.set_intersect (pat_vars p) out in
  -            if BU.set_is_empty intersection
  -            then BU.set_union out (pat_vars p)
  -            else
  -              let duplicate_bv = List.hd (BU.set_elements intersection) in
  -              raise_error ( Errors.Fatal_NonLinearPatternNotPermitted,
  -                            BU.format1
  -                              "Non-linear patterns are not permitted: `%s` appears more than once in this pattern."
  -                               (duplicate_bv.ppname.idText) )
  -
  -                          r
  -        in
  -        List.fold_left aux S.no_names pats
  -    in
  -
  -    // check that the same variables are bound in each pattern
  -    match pats with
  -    | [] -> ()
  -    | [p] -> pat_vars p |> ignore
  -    | p::ps ->
  -      let pvars = pat_vars p in
  -      let aux p =
  -        if BU.set_eq pvars (pat_vars p) then () else
  -        let nonlinear_vars = BU.set_symmetric_difference pvars (pat_vars p) in
  -        let first_nonlinear_var = List.hd (BU.set_elements nonlinear_vars) in
  -        raise_error ( Errors.Fatal_IncoherentPatterns,
  -                      BU.format1
  -                        "Patterns in this match are incoherent, variable %s is bound in some but not all patterns."
  -                         (first_nonlinear_var.ppname.idText) )
  -                    r
  -      in
  -      List.iter aux ps
  -  in // /check_linear_pattern_variables pats
  -
     let resolvex (l:lenv_t) e x =
       match l |> BU.find_opt (fun y -> y.ppname.idText=x.idText) with
         | Some y -> l, e, y
  
positive.code:         (x::l), e, x
    in
  
    let rec aux' (top:bool) (loc:lenv_t) env (p:pattern)
      : lenv_t                         (* list of all BVs mentioned *)
      * env_t                          (* env updated with the BVs pushed in *)
      * bnd                            (* a binder for the pattern *)
  
negative.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 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
  