anchor.diff:  
           | _ -> mlAppExpr
   
  -let check_pats_for_ite (l:list<(pat * option<term> * term)>) :(bool * option<term> * option<term>) =
  -    let def = false, None, None in
  -    if List.length l <> 2 then def
  -    else
  -        let (p1, w1, e1) = List.hd l in
  -        let (p2, w2, e2) = List.hd (List.tl l) in
  -        match (w1, w2, p1.v, p2.v) with
  -            | (None, None, Pat_constant (Const_bool true), Pat_constant (Const_bool false)) -> true, Some e1, Some e2
  -            | (None, None, Pat_constant (Const_bool false), Pat_constant (Const_bool true)) -> true, Some e2, Some e1
  -            | _ -> def
  -
  -type univ = 
  -    | Term
  -    | UZero
  -    | UPlus
  -
  -let predecessor = function
  -    | Term -> failwith "Impossible"
  -    | UZero -> Term
  -    | UPlus -> UZero
  -     
  -let rec univ t = 
  -    match (SS.compress t).n with 
  -        | Tm_delayed _
  -        | Tm_unknown -> 
  -          failwith "Impossible"
  -
  -        | Tm_constant _ -> 
  -          Term
  -
  -        | Tm_bvar x 
  -        | Tm_name x ->
  -          predecessor <| univ x.sort 
  -
  -        | Tm_fvar fv -> 
  -          predecessor <| univ fv.fv_name.ty
  -
  -        | Tm_ascribed(_, t, _) -> 
  -          predecessor <| univ t
  -
  -        | Tm_type _ -> 
  -          UPlus
  -
  -        | Tm_uvar (_, t) -> 
  -          predecessor <| univ t
  -           
  -        | Tm_uinst(t, _) -> 
  -          univ t
  -
  -        | Tm_refine(x, _) -> 
  -          predecessor <| univ t
  -
  -        | Tm_arrow(bs, c) -> 
  -          univ (U.comp_result c)
  -
  -        | Tm_abs(_, _, Some c) -> 
  -          predecessor <| univ c.res_typ
  -       
  -        | Tm_abs(bs, body, None) -> 
  -          univ body
  -
  -        | Tm_let(_, body) -> 
  -          univ body
  -
  -        | Tm_match(_, branches) -> 
  -          begin match branches with 
  -            | (_, _, e)::_ -> univ e
  -            | _ -> failwith "Empty branches"
  -          end
  -
  -        | Tm_meta(t, _) -> 
  -          univ t
  -
  -        | Tm_app(head, _) -> 
  -          univ head
  -
  -let is_type t = match univ t with 
  -    | Term -> false
  -    | _ -> true
  -
  -let is_type_binder x = 
  -    match univ (fst x).sort with 
  -    | Term -> failwith "Impossible"
  -    | UZero -> false
  -    | UPlus -> true
  -
  +
  +//The main extraction function
   let rec check_term (g:env) (t:term) (f:e_tag) (ty:mlty) :  (mlexpr * mlty) =
       // debug g (fun () -> printfn "Checking %s at type %A\n" (Print.exp_to_string e) t);
       let e, t = check_term' g t f ty in
  
positive.code:           extraction-preimage is definitionally equal in F* to that of mlAppExpr
         2) meets the ML requirements that the args to datacons be tupled 
            and that the datacons be fully applied
  *)
  let maybe_lalloc_eta_data (g:env) (qual : option<fv_qual>) (residualType : mlty)  (mlAppExpr : mlexpr) : mlexpr =
      let rec eta_args more_args t = match t with
          | MLTY_Fun (t0, _, t1) ->
            let x = gensym () in
  
negative.code: 
  (* something is a value iff it qualifies for the OCaml's "value restriction", 
     which determines when a definition can be generalized *)
  let rec is_fstar_value (t:term) =   
      match (SS.compress t).n with
      | Tm_constant _
      | Tm_bvar _
  