anchor.diff:  
   let mkAccuVar (v:var) = Accu(Var v, [])
   let mkAccuMatch (s : t) (c : t -> t) = Accu(Match (s, c), [])
  -let mkAccuRec (b:letbinding) (env:list<t>) = Accu(Rec(b, env), [])
  +let mkAccuRec (b:letbinding) (bs:list<letbinding>) (env:list<t>) = Accu(Rec(b, bs, env), [])
   
   let isAccu (trm:t) =
     match trm with
  
positive.code:      (match elt with
        | Some { sigel = Sig_let ((is_rec, [lb]), _) } ->
          if is_rec then
            mkAccuRec lb []
          else
            begin
               debug (fun() -> BU.print "Translate fv: it's a Sig_let\n" []);
  
negative.code:     | Univ u -> u
      | _ -> failwith "Not a universe"
  
  
  (* Creates the environment of mutually recursive function definitions *)
  let make_rec_env (lbs:list<letbinding>) (bs:list<t>) : list<t> = 
    let rec aux (lbs:list<letbinding>) (lbs0:list<letbinding>) (bs:list<t>) (bs0:list<t>) : list<t> = 
    match lbs with 
    | [] -> bs
    | lb::lbs' -> aux lbs' lbs0 ((mkAccuRec lb lbs0 bs0) :: bs) bs0
    in 
    aux lbs lbs bs bs
  
  (* We are not targeting tagless normalization at this point *)
  let rec app (f:t) (x:t) (q:aqual) =
    debug (fun () -> BU.print2 "When creating app: %s applied to %s\n" (t_to_string f) (t_to_string x));
  