anchor.diff:          // what's up with that?
           // GM: I actually get a regression if I just keep the second branch.
           if not cfg.steps.iota
  -        then if cfg.steps.hnf
  +        then if cfg.steps.hnf && not (is_partial_primop_app cfg t)
                then let arg = closure_as_term cfg env_arg tm in
                     let t = extend_app t (arg, aq) None r in
                     rebuild cfg env_arg stack t
  
positive.code:                   norm cfg env_arg stack tm
          else begin match !m with
            | None ->
              if cfg.steps.hnf
              then let arg = closure_as_term cfg env_arg tm in
                   let t = extend_app t (arg, aq) None r in
                   rebuild cfg env_arg stack t
  
negative.code:       Some f
      | _ -> None)
    | _ -> None
  
  (* Returns `true` iff the head of `t` is a primop, and
  it not applied or only partially applied. *)
  let is_partial_primop_app (cfg:Cfg.cfg) (t:term) : bool =
    let hd, args = U.head_and_args t in
    match (U.un_uinst hd).n with
    | Tm_fvar fv ->
      begin match find_prim_step cfg fv with
      | Some prim_step -> prim_step.arity > List.length args
      | None -> false
      end
    | _ -> false
  
  (* GM: Please consider this function private outside of this recursive
   * group, and call `normalize` instead. `normalize` will print timing
  