diff --git a/src/library/tactic/dsimplify.cpp b/src/library/tactic/dsimplify.cpp
index 01f0348fc0..d8a11ce573 100644
--- a/src/library/tactic/dsimplify.cpp
+++ b/src/library/tactic/dsimplify.cpp
@@ -311,7 +311,7 @@ vm_obj tactic_dsimplify_core(vm_obj const &, vm_obj const & a,
                              vm_obj const & pre, vm_obj const & post, vm_obj const & e, vm_obj const & _s) {
     tactic_state const & s = to_tactic_state(_s);
     try {
-        type_context ctx = mk_type_context_for(s);
+        type_context ctx = mk_type_context_for(s, transparency_mode::Reducible);
         defeq_can_state dcs = s.dcs();
         tactic_dsimplify_fn F(ctx, dcs, force_to_unsigned(max_steps, std::numeric_limits<unsigned>::max()),
                               to_bool(visit_instances), a, pre, post);
@@ -327,7 +327,7 @@ vm_obj simp_lemmas_dsimplify_core(vm_obj const & max_steps, vm_obj const & visit
                                   vm_obj const & e, vm_obj const & _s) {
     tactic_state const & s = to_tactic_state(_s);
     try {
-        type_context ctx    = mk_type_context_for(s);
+        type_context ctx    = mk_type_context_for(s, transparency_mode::Reducible);
         defeq_can_state dcs = s.dcs();
         simp_lemmas_for dlemmas;
         if (auto * dls = to_simp_lemmas(lemmas).find(get_eq_name()))
diff --git a/tests/lean/1327.lean b/tests/lean/1327.lean
new file mode 100644
index 0000000000..dcee0c2055
--- /dev/null
+++ b/tests/lean/1327.lean
@@ -0,0 +1,4 @@
+example (n) : nat.pred n = n :=
+begin
+  dsimp
+end
diff --git a/tests/lean/1327.lean.expected.out b/tests/lean/1327.lean.expected.out
new file mode 100644
index 0000000000..75d6171788
--- /dev/null
+++ b/tests/lean/1327.lean.expected.out
@@ -0,0 +1,4 @@
+1327.lean:4:0: error: tactic failed, there are unsolved goals
+state:
+n : ℕ
+⊢ nat.pred n = n
diff --git a/tests/lean/defeq_simp1.lean b/tests/lean/defeq_simp1.lean
index 6413421877..8542b9ff63 100644
--- a/tests/lean/defeq_simp1.lean
+++ b/tests/lean/defeq_simp1.lean
@@ -1,6 +1,6 @@
-attribute [reducible]
-definition nat_has_add2 : has_add nat :=
-has_add.mk (λ x y : nat, x + y)
+@[reducible]
+def nat_has_add2 : has_add nat :=
+⟨λ x y : nat, nat.add x y⟩
 
 set_option pp.all true
 
diff --git a/tests/lean/run/destruct.lean b/tests/lean/run/destruct.lean
index 5f8a4c8146..0448a9cca3 100644
--- a/tests/lean/run/destruct.lean
+++ b/tests/lean/run/destruct.lean
@@ -25,6 +25,6 @@ example : ∀ n, 0 < n → succ (pred n) = n :=
 begin
   intro n,
   destruct n,
-   dsimp, intros, note h := lt_irrefl 0, cc,
-   dsimp, intros, subst n
+   {dsimp, intros, note h := lt_irrefl 0, cc},
+   {intros, subst n, dsimp, reflexivity}
 end