diff --git a/src/library/blast/backward/backward_lemmas.cpp b/src/library/blast/backward/backward_lemmas.cpp
index b978dcae9..3738ea860 100644
--- a/src/library/blast/backward/backward_lemmas.cpp
+++ b/src/library/blast/backward/backward_lemmas.cpp
@@ -60,9 +60,9 @@ typedef scoped_ext<backward_config> backward_ext;
 static optional<head_index> get_backward_target(tmp_type_context & ctx, expr type) {
     while (is_pi(type)) {
         expr local = ctx.mk_tmp_local(binding_domain(type));
-        type = ctx.try_to_pi(instantiate(binding_body(type), local));
+        type = ctx.whnf(instantiate(binding_body(type), local));
     }
-    expr fn = get_app_fn(ctx.whnf(type));
+    expr fn = get_app_fn(type);
     if (is_constant(fn) || is_local(fn))
         return optional<head_index>(fn);
     else
diff --git a/src/library/blast/grinder/intro_elim_lemmas.cpp b/src/library/blast/grinder/intro_elim_lemmas.cpp
index ee9582621..2ab1cbe5b 100644
--- a/src/library/blast/grinder/intro_elim_lemmas.cpp
+++ b/src/library/blast/grinder/intro_elim_lemmas.cpp
@@ -80,9 +80,9 @@ optional<name> get_intro_target(tmp_type_context & ctx, name const & c) {
     expr type = ctx.try_to_pi(instantiate_type_univ_params(d, to_list(us)));
     while (is_pi(type)) {
         expr local = ctx.mk_tmp_local(binding_domain(type));
-        type = ctx.try_to_pi(instantiate(binding_body(type), local));
+        type = ctx.whnf(instantiate(binding_body(type), local));
     }
-    expr const fn = get_app_fn(ctx.whnf(type));
+    expr const fn = get_app_fn(type);
     if (is_constant(fn))
         return optional<name>(const_name(fn));
     else