anchor.diff:                     | BU.Inl bv -> S.bv_to_name bv
                      | BU.Inr fv -> failwith "Not yet implemented"
              in
  -           S.mk (Tm_let((true, [lb]), f)) None Range.dummyRange
  +           S.mk (Tm_let((true, lbs), f)) None Range.dummyRange
            in
            let args = map_rev (fun (x, q) -> (readback env x, q)) ts in
            (match ts with
  
positive.code:       in
        case (translate env bs scrut)
  
      | Tm_let((false, [lb]), body) -> // non-recursive let
        let def = translate_letbinding env bs lb 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 *)
  
      | Tm_let _ -> failwith "Mutual recursion; not yet handled"
  
  
negative.code:        | [] -> head
         | _ -> U.mk_app head args)
  
      | Accu (Rec(lb, lbs, bs), ts) ->
         let rec curry hd args =
         match args with
         | [] -> hd
  