anchor.diff:  open FStar
   open FStar.TypeChecker
   open FStar.Syntax.Syntax
  -
  +open FStar.Ident
  +  
   module S = FStar.Syntax.Syntax
   module SS = FStar.Syntax.Subst
   module Range = FStar.Range
  
positive.code: module BU = FStar.Util
  module Env = FStar.TypeChecker.Env
  
  (* Utils *)
  
  // VD: This seems necessary for the OCaml build
  
negative.code:     | Tm_abs ([x], body, _) ->
        Lam (fun (y:t) -> translate env (y::bs) body)
  
      | Tm_fvar fvar ->
        let find_in_sigtab (env : Env.env) (lid : lident) : option<sigelt> = BU.smap_try_find env.sigtab (text_of_lid lid) in
        (match find_in_sigtab env fvar.fv_name.v with 
         | Some elt ->
           (match elt.sigel with 
            | Sig_datacon _ -> mkConstruct fvar []
            | Sig_inductive_typ _ -> mkAccInd fvar
            | _ -> failwith "Sigelt not yet supported")
         | None -> failwith "Free variable not found")
      | Tm_abs (x::xs, body, _) ->
        let rest = S.mk (Tm_abs(xs, body, None)) None Range.dummyRange in
        let tm = S.mk (Tm_abs([x], rest, None)) None e.pos in
  