anchor.diff:  and atom_to_string (a: atom) =
       match a with
       | Var v -> "Var " ^ (P.bv_to_string v)
  -    | Match (t, _, _) -> "Match " ^ (t_to_string t)
  +    | Match (t, _) -> "Match " ^ (t_to_string t)
       | Rec (_,_, l) -> "Rec (" ^ (String.concat "; " (List.map t_to_string l)) ^ ")"
   
   let is_not_accu (x:t) =
  
positive.code: let mkConstruct i us ts = Construct(i, us, ts)
  
  let mkAccuVar (v:var) = Accu(Var v, [])
  let mkAccuMatch (s:t) (c:t -> t) (bs:((t -> term) -> list<branch>)) = Accu(Match (s, c, bs), [])
  let mkAccuRec (b:letbinding) (bs:list<letbinding>) (env:list<t>) = Accu(Rec(b, bs, env), [])
  
  let isAccu (trm:t) =
  
negative.code: type atom = //JUST FSHARP
    | Var of var
    | Match of t * (* the scutinee *)
               ((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
  