anchor.diff:                       else None)
   
   (* uncurried application *)
  -let rec iapp cfg (f:t) (args:args) : t =
  -  debug cfg (fun () -> BU.print2 "App : %s @ (%s)\n" (t_to_string f) (args_to_string args));
  +let rec iapp (f:t) (args:args) : t =
     match f with
     | Lam (f, targs, n) ->
       let m = List.length args in
  
positive.code:     | Tm_uinst(t, us) ->
        debug (fun () -> BU.print2 "Uinst term : %s\nUnivs : %s\n" (P.term_to_string t)
                                                                (List.map P.univ_to_string us |> String.concat ", "));
        iapp cfg (translate cfg bs t) (List.map (fun x -> as_arg (Univ (translate_univ bs x))) us)
  
      | Tm_type u ->
        Type_t (translate_univ bs u)
  
negative.code:               | Some x -> debug (fun () -> BU.print2 "Primitive operator %s returned %s\n" (P.fv_to_string fvar) (t_to_string x));
                           x
                | None -> debug (fun () -> BU.print1 "Primitive operator %s failed\n" (P.fv_to_string fvar)); 
                         iapp (mkFV fvar [] []) args'),
                (let f (_:int) () : t * S.aqual = (Constant Unit, None) in tabulate arity f),
                arity)
  
  