anchor.diff:             in
              S.mk (Tm_let((true, [lb]), f)) None Range.dummyRange
            in
  -         let args = map_rev (fun x -> as_arg (readback x)) ts in
  +         let args = map_rev (fun x -> as_arg (readback env x)) ts in
            (match ts with 
             | [] -> head
             | _ -> U.mk_app head args)
  
positive.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 ((List.rev args) @ bs) (pickBranch c branches) in
            branch
          | _ -> 
            mkAccuMatch scrut case
        in 
        case (translate bs scrut)
  
      | Tm_let((false, [lb]), body) -> // non-recursive let
        let def = translate bs lb.lbdef in
        translate (def::bs) body
  
      | Tm_let((true, [lb]), body) -> // recursive let with only one recursive definition
        let f = mkAccuRec lb bs in 
        translate (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 
  
negative.code: //         | _ -> failwith "Recursive definition not a function")
  // >>>>>>> 86f93ae6edc257258f376954fed7fba11f53ff83
  
  let normalize (env : Env.env) (e:term) : term = readback env (translate env [] e)
  