anchor.diff:        translate (def::bs) body
   
       | Tm_let((true, [lb]), body) -> // recursive let with only one recursive definition
  +      let f = Rec (lb.lbdef, 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 
         // let fnorm f = translate (f::bs) def in
         // let rec f = fnorm f in
         // translate (f::bs) body
  -      failwith "Not yet implemented"
  +      //failwith "Not yet implemented"
         
       | _ -> debug_term e; failwith "Not yet implemented"
   
  
positive.code:     branch :: mkBranches branches' cont
    | _ -> failwith "Unexpected pattern" 
  
  let rec translate (bs:list<t>) (e:term) : t =
      match (SS.compress e).n with
      | Tm_delayed _ -> failwith "Impossible"
  
  
negative.code:       (match ts with 
         | [] -> head
         | _ -> U.mk_app head args)
      | Accu (FiX t, ts) -> failwith "Not yet implemented"
                            (* Danel: hmm, should we wrap this stuck 
                               application inside a (unary) let rec? *)
      | _ -> failwith "Not yet implemented"
      
  let normalize (e:term) : term = readback (translate [] e)
  