anchor.diff:  let try_unembed  (e:embedding<'a>) t n = unembed e t false n
   let type_of     (e:embedding<'a>)     = e.typ
   
  -let lazy_embed rng ta (x:'a) (f:unit -> term) =
  +let lazy_embed (pa:printer<'a>) rng ta (x:'a) (f:unit -> term) =
  +    let thunk = FStar.Common.mk_thunk f in
  +    let tm = FStar.Common.force_thunk thunk in
  +    //BU.print3 "Embedding a %s\n\tvalue is %s\nthunked as a %s\n"
  +    //            (Print.term_to_string ta)
  +    //            (pa x)
  +    //            (Print.term_to_string tm);
       S.mk (Tm_lazy({blob=FStar.Dyn.mkdyn x;
                      ltyp=S.tun;
                      rng=rng;
  -                   lkind=Lazy_embedding (ta, FStar.Common.mk_thunk f)}))
  +                   lkind=Lazy_embedding (ta, thunk)}))
            None
            rng
   
  -let lazy_unembed (x:term) (ta:term) (f:term -> option<'a>) : option<'a> =
  +let lazy_unembed (pa:printer<'a>) (x:term) (ta:term) (f:term -> option<'a>) : option<'a> =
       let x = SS.compress x in
       match x.n with
  -    | Tm_lazy {blob=b; lkind=Lazy_embedding (tb, _)} ->
  -      BU.print2 "Unembedding a %s as a %s\n" (Print.term_to_string tb) (Print.term_to_string ta);
  -      Some (FStar.Dyn.undyn b)
  +    | Tm_lazy {blob=b; lkind=Lazy_embedding (tb, t)}  ->
  +      let a = FStar.Dyn.undyn b in
  +      let tm = FStar.Common.force_thunk t in
  +      //BU.print3 "Unembedding a %s as a %s\n unthunked a %s\n"
  +      //          (Print.term_to_string tb)
  +      //          (Print.term_to_string ta)
  +      //          (Print.term_to_string tm);
  +      //(match f tm with
  +      // | None -> ()
  +      // | Some a' ->
  +      //   //if (a <> a')
  +      //   //then failwith (BU.format2 "Unembedding is inconsistent:\n\texpected %s\n\tgot %s\n" (pa a') (pa a));
  +      //   BU.print_string "Successful unembedding\n"
  +      // );
  +       Some a
       | _ -> f x
   
   let e_any =
  
positive.code:             Err.log_issue t0.pos (Err.Warning_NotEmbedded, BU.format1 "Not an embedded char: %s" (Print.term_to_string t0));
              None
      in
      mk_emb em un S.t_char
  
  let e_int =
      let t_int = U.fvar_const PC.int_lid in
      let em (i:Z.t) (rng:range) _topt _norm : term =
          lazy_embed rng t_int i (fun () -> U.exp_int (Z.string_of_big_int i))
      in
      let un (t0:term) (w:bool) _norm : option<Z.t> =
          let t = U.unmeta_safe t0 in
          lazy_unembed t t_int (fun t ->
              match t.n with
              | Tm_constant(FStar.Const.Const_int (s, _)) ->
                  Some (Z.big_int_of_string s)
  
negative.code:     in
      let un (t0:term) (w:bool) norm : option<('a * 'b)> =
          let t = U.unmeta_safe t0 in
          lazy_unembed printer t t_pair_a_b (fun t ->
          let hd, args = U.head_and_args t in
          match (U.un_uinst hd).n, args with
          | Tm_fvar fv, [_; _; (a, _); (b, _)] when S.fv_eq_lid fv PC.lid_Mktuple2 ->
  