anchor.diff:  
   let e_norm_step =
       let t_norm_step = U.fvar_const (Ident.lid_of_str "FStar.Syntax.Embeddings.norm_step") in
  +    let printer _ = "norm_step" in
       let em (n:norm_step) (rng:range) _topt norm : term =
  -        lazy_embed rng t_norm_step n (fun () ->
  +        lazy_embed printer rng t_norm_step n (fun () ->
           match n with
           | Simpl ->
               steps_Simpl
  
positive.code:             Err.log_issue t0.pos (Err.Warning_NotEmbedded, BU.format1 "Not an embedded list: %s" (Print.term_to_string t0));
              None)
      in
      mk_emb em un (S.t_list_of (type_of ea))
  
  let e_string_list = e_list e_string
  
  
negative.code:                 Err.log_issue t0.pos (Err.Warning_NotEmbedded, (BU.format1 "Not an embedded int: %s" (Print.term_to_string t0)));
                  None)
      in
      mk_emb_with_printer em un S.t_int BigInt.string_of_big_int
  
  let e_string =
      let em (s:string) (rng:range) _topt _norm : term =
  