anchor.diff:      in
       { NBETerm.em = embed_result
       ; NBETerm.un = unembed_result
  -    ; NBETerm.typ = mkFV fv_result [] []
  -    ; NBETerm.emb_typ = fv_as_emb_typ fv_result }
  +    ; NBETerm.typ = mkFV fstar_tactics_result.fv [] []
  +    ; NBETerm.emb_typ = fv_as_emb_typ fstar_tactics_result.fv }
   
   
   let e_direction =
       let embed_direction (rng:Range.range) (d : direction) : term =
           match d with
  -        | TopDown -> fstar_tactics_topdown
  -        | BottomUp -> fstar_tactics_bottomup
  +        | TopDown -> fstar_tactics_topdown.t
  +        | BottomUp -> fstar_tactics_bottomup.t
       in
       let unembed_direction w (t : term) : option<direction> =
           match (SS.compress t).n with
  -        | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_topdown_lid -> Some TopDown
  -        | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_bottomup_lid -> Some BottomUp
  +        | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_topdown.lid -> Some TopDown
  +        | Tm_fvar fv when S.fv_eq_lid fv fstar_tactics_bottomup.lid -> Some BottomUp
           | _ ->
               if w then
                   Err.log_issue t.pos (Err.Warning_NotEmbedded, (BU.format1 "Not an embedded direction: %s" (Print.term_to_string t)));
               None
       in
  -    mk_emb embed_direction unembed_direction t_direction
  +    mk_emb embed_direction unembed_direction fstar_tactics_direction.t
   
   let e_direction_nbe  =
       let embed_direction cb (res:direction) : NBET.t =
           match res with
  -        | TopDown  -> mkConstruct fstar_tactics_topdown_fv [] []
  -        | BottomUp -> mkConstruct fstar_tactics_bottomup_fv [] []
  +        | TopDown  -> mkConstruct fstar_tactics_topdown.fv [] []
  +        | BottomUp -> mkConstruct fstar_tactics_bottomup.fv [] []
       in
       let unembed_direction cb (t:NBET.t) : option<direction> =
           match t with
  -        | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_topdown_lid -> Some TopDown
  -        | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_bottomup_lid -> Some BottomUp
  +        | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_topdown.lid -> Some TopDown
  +        | NBETerm.Construct (fv, _, []) when S.fv_eq_lid fv fstar_tactics_bottomup.lid -> Some BottomUp
           | _ ->
             if !Options.debug_embedding then
               Err.log_issue Range.dummyRange (Err.Warning_NotEmbedded, (BU.format1 "Not an embedded direction: %s" (NBETerm.t_to_string t)));
  
positive.code:     let embed_result (res:__result<'a>) (rng:Range.range) _ _ : term =
          match res with
          | Success (a, ps) ->
            S.mk_Tm_app (S.mk_Tm_uinst fstar_tactics_Success_tm [U_zero])
                   [S.iarg (type_of ea);
                    S.as_arg (embed ea rng a);
                    S.as_arg (embed e_proofstate rng ps)]
                   None rng
          | Failed (e, ps) ->
            S.mk_Tm_app (S.mk_Tm_uinst fstar_tactics_Failed_tm [U_zero])
                   [S.iarg (type_of ea);
                    S.as_arg (embed e_exn rng e);
                    S.as_arg (embed e_proofstate rng ps)]
  
negative.code: 
  let e_proofstate =
      let embed_proofstate (rng:Range.range) (ps:proofstate) : term =
          U.mk_lazy ps fstar_tactics_proofstate.t Lazy_proofstate (Some rng)
      in
      let unembed_proofstate w (t:term) : option<proofstate> =
          match (SS.compress t).n with
  