anchor.diff:                               | Some ats, Some ats' -> BU.for_some (fun at -> BU.for_some (U.attr_eq at) ats') ats
                                | _, _ -> false)))
                    in
  -                 log cfg (fun () -> BU.print3 ">>> For %s (%s), should_delta = %s\n"
  +                 log cfg (fun () -> 
  +                     // printfn "cfg.delta_level = %A" cfg.delta_level;
  +                     BU.print3 ">>> For %s (%s), should_delta = %s\n"
                                    (Print.term_to_string t)
                                    (Range.string_of_range t.pos)
                                    (string_of_bool should_delta));
  
positive.code:     let t = S.extend_app head (t,aq) None r in
      rebuild cfg env stack t
  
    | Match(env, branches, r) :: stack ->
      log cfg  (fun () -> BU.print1 "Rebuilding with match, scrutinee is %s ...\n" (Print.term_to_string t));
      //the scrutinee is always guaranteed to be a pure or ghost term
      //see tc.fs, the case of Tm_match and the comment related to issue #594
  
negative.code:       // If either Weak or HNF, then don't descend into branch
        let whnf = cfg.steps.weak || cfg.steps.hnf in
        let cfg_exclude_iota_zeta =
          // let new_delta =
          //   cfg.delta_level |> List.filter (function
          //     | Env.Inlining
          //     | Env.Eager_unfolding_only -> true
          //     | _ -> false)
          // in
          ({cfg with steps= { cfg.steps with zeta = false }; strong=true})
        in
        let norm_or_whnf env t =
          if whnf
  