anchor.diff:    | [] -> cnt <= 0 
     | t :: ts -> (not (isAccu t)) && test_args ts (cnt - 1)
   
  -(* It count the number of abstractions in the body of a let rec. 
  +(* Count the number of abstractions in the body of a let rec. 
      It accounts for abstractions instantiated inside the body.
      This analysis needs further refinement, for example see the let in case. 
   *)
  
positive.code:            in
             S.mk (Tm_let((true, [lb]), f)) None Range.dummyRange
           in
           let args = map_rev (fun x -> as_arg (readback x)) ts in
           (match ts with 
            | [] -> head
            | _ -> U.mk_app head args)
  
negative.code:           (* Assuming that all the arguments to the pattern constructors 
               are binders -- i.e. no nested patterns for now  *) 
            (* XXX : is rev needed? *)
            let branch = translate env ((List.rev args) @ bs) (pickBranch c branches) in
            branch
          | _ -> 
            mkAccuMatch scrut case
        in 
        case (translate env bs scrut)
  
      | Tm_let((false, [lb]), body) -> // non-recursive let
        let def = translate env bs lb.lbdef in
        translate env (def::bs) body
  
      | Tm_let((true, [lb]), body) -> // recursive let with only one recursive definition
        let f = mkAccuRec lb bs in 
        translate env (f::bs) body (* Danel: storing the rec. def. as F* code wrapped in a thunk *)
  
        // this will loop infinitely when the recursive argument is symbolic 
        // let def = lb.lbdef in 
  