diff --git a/src/library/blast/backward/backward_strategy.cpp b/src/library/blast/backward/backward_strategy.cpp
index bbd5293f8..75d4d7d3f 100644
--- a/src/library/blast/backward/backward_strategy.cpp
+++ b/src/library/blast/backward/backward_strategy.cpp
@@ -71,7 +71,6 @@ class backward_strategy : public strategy {
         Try(assumption_action());
         list<gexpr> backward_rules = get_extension().get_backward_rule_set().find(head_index(curr_state().get_target()));
         Try(backward_action(backward_rules, true));
-        Try(constructor_action());
         return action_result::failed();
     }
 };
diff --git a/tests/lean/run/blast20.lean b/tests/lean/run/blast20.lean
index aad048516..70ba0de36 100644
--- a/tests/lean/run/blast20.lean
+++ b/tests/lean/run/blast20.lean
@@ -12,6 +12,8 @@ by blast
 example : ∀ (F F' : Prop), F ∧ F' → F :=
 by blast
 
+attribute and.intro [backward]
+
 example : ∀ (P Q R : nat → Prop) (F : Prop), (F ∧ (∀ n m, (Q m ∧ R n) → P n)) →
             (F → R 2) → Q 1 → P 2 ∧ F :=
 by blast