anchor.diff:  type atom = //JUST FSHARP
     | Var of var
     | Match of t * (* the scutinee *)
  -             (t -> t) * (* the closure that pattern matches the scrutiny *)
  -             list<branch> 
  +             (t -> t) * (* the computation that pattern matches the scrutiny *)
  +             ((t -> term) -> list<branch>) (* the computation that reconstructs the pattern matching, parameterized by the readback function *)
                // ZP: Keep the original branches to reconstruct just the patterns
                // NS: add a thunked pattern translations here
     | Rec of letbinding * list<letbinding> * list<t> (* Danel: This wraps a unary F* rec. def. as a thunk in F# *)
  
positive.code:       let args = map_rev (fun (x, q) -> (readback env x, q)) ts in
        U.mk_app (S.bv_to_name bv) args
  
      | Accu (Match (scrut, cases, branches), ts) ->
        let args = map_rev (fun (x, q) -> (readback env x, q)) ts in
        let head = 
          let scrut_new = readback env scrut in
          let branches_new = 
            List.map (fun (pat, when_clause, _) -> pat, when_clause, readback env (cases (translate_pat pat))) 
                     branches 
          in
          S.mk (Tm_match (scrut_new, branches_new)) None Range.dummyRange
        in
        (*  When `cases scrut` returns a Accu(Match ..))
  
negative.code:           | Some (branch, args) ->
              translate env (List.fold_left (fun bs x -> x::bs) bs args) branch
            | None -> //no branch is determined
              mkAccuMatch scrut case patterns
            end
          | Constant c ->
            (* same as for construted values, but args are either empty or is a singleton list (for wildcard patterns) *)
  