anchor.diff:  let lookup_free_var_sym env a =
       let name, sym, zf_opt = lookup_lid env a.v in
       match zf_opt with
  -        | Some({tm=App(g, zf)}) when env.use_zfuel_name -> g, zf
  -        | _ ->
  -            match sym with
  -                | None -> Var name, []
  -                | Some sym ->
  -                    match sym.tm with
  -                        | App(g, [fuel]) -> g, [fuel]
  -                        | _ -> Var name, []
  +    | Some mkf when env.use_zfuel_name ->
  +      begin match (mkf 0).tm with
  +        | App(g, zf) -> g, zf
  +        | _ -> failwith "Impossible"
  +      end
  +    | _ ->
  +      match sym with
  +      | None -> Var name, []
  +      | Some sym ->
  +        match sym.tm with
  +        | App(g, [fuel]) -> g, [fuel]
  +        | _ -> Var name, []
   
   let tok_of_name env nm =
       BU.find_map env.bindings (function
  
positive.code:             match (U.un_uinst head).n, args with
                  | Tm_fvar fv, [(e, _)] when S.fv_eq_lid fv Const.smtpatOr_lid ->
                    Some e
                  | _ -> None in
          match elts with
              | [t] ->
               begin match smt_pat_or t with
  
negative.code:     let one_pat p =
          let head, args = U.unmeta p |> U.head_and_args in
          match (U.un_uinst head).n, args with
          | Tm_fvar fv, [(_, _); (e, _)] when S.fv_eq_lid fv Const.smtpat_lid -> e
          | Tm_fvar fv, [(e, _)] when S.fv_eq_lid fv Const.smtpatT_lid -> e
          | _ -> failwith "Unexpected pattern term"
      in
  
      let lemma_pats p =
          let elts = list_elements p in
  