anchor.diff:        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
  
positive.code:         // 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 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:                   norm cfg env_arg stack tm
          else begin match !m with
            | None ->
              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
  