anchor.diff:             | Some (branch, [arg]) ->
                translate env (arg::bs) branch
              | None -> //no branch is determined
  -             mkAccuMatch scrut case branches
  +             mkAccuMatch scrut case patterns
              | Some (_, hd::tl) -> failwith "Impossible: Matching on constants cannot bind more than one variable")
   
           | _ ->
  -          mkAccuMatch scrut case branches
  +          mkAccuMatch scrut case patterns
  +      (* Thunked computation that reconstructs the patterns *)
  +      and patterns (readback:t -> term) : list<branch> = 
  +        let rec process_pattern (p:pat) : pat = 
  +          let p_new = 
  +            match p.v with
  +            | Pat_constant c -> Pat_constant c
  +            | Pat_cons (fvar, args) -> Pat_cons (fvar, List.map (fun (p, b) -> (process_pattern p, b)) args)
  +            | Pat_var bvar -> Pat_var {bvar with sort = readback (translate env bs bvar.sort)}
  +            | Pat_wild bvar -> Pat_wild {bvar with sort = readback (translate env bs bvar.sort)}
  +            (* Zoe: I'm not sure what this is, just speculating the translation *)
  +            | Pat_dot_term (bvar, tm) -> Pat_dot_term ({bvar with sort = readback (translate env bs bvar.sort)}, readback (translate env bs tm))
  +          in
  +          {p with v = p_new} (* keep the info and change the pattern *) 
  +        in
  +        List.map (fun (pat, when_clause, _) -> process_pattern pat, when_clause, readback (case (translate_pat pat))) 
  +                 branches 
         in
         case (translate env bs scrut)
   
  
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) *)
  