diff --git a/src/library/type_context.cpp b/src/library/type_context.cpp
index 3ea8f921a3..4a06a9d071 100644
--- a/src/library/type_context.cpp
+++ b/src/library/type_context.cpp
@@ -278,16 +278,6 @@ pair<local_context, expr> type_context::revert_core(buffer<expr> & to_revert, lo
     unsigned num   = to_revert.size();
     if (num == 0)
         return mk_pair(ctx, type);
-    /* Check whether we are trying to revert a frozen local instance. */
-    if (optional<local_instances> lis = m_lctx.get_frozen_local_instances()) {
-        for (expr const & h : to_revert) {
-            for (local_instance const & li : *lis) {
-                if (mlocal_name(h) == mlocal_name(li.get_local())) {
-                    throw exception(sstream() << "failed to revert '" << h << "', it is a frozen local instance (possible solution: use tactic `tactic.unfreeze_local_instances` to reset the set of local instances)");
-                }
-            }
-        }
-    }
     local_decl d0     = get_local_with_smallest_idx(ctx, to_revert);
     bool must_sort    = false;
     process_to_revert(m_mctx, to_revert, num, d0, preserve_to_revert_order, must_sort);
@@ -327,6 +317,16 @@ pair<local_context, expr> type_context::revert_core(buffer<expr> & to_revert, lo
                 return ctx.get_local_decl(l1).get_idx() < ctx.get_local_decl(l2).get_idx();
             });
     }
+    /* Check whether we are trying to revert a frozen local instance. */
+    if (optional<local_instances> lis = m_lctx.get_frozen_local_instances()) {
+        for (expr const & h : to_revert) {
+            for (local_instance const & li : *lis) {
+                if (mlocal_name(h) == mlocal_name(li.get_local())) {
+                    throw exception(sstream() << "failed to revert '" << h << "', it is a frozen local instance (possible solution: use tactic `tactic.unfreeze_local_instances` to reset the set of local instances)");
+                }
+            }
+        }
+    }
     local_context new_ctx = ctx.remove(to_revert);
     return mk_pair(new_ctx, mk_pi(ctx, to_revert, type));
 }
diff --git a/tests/lean/revert_frozen_dep.lean b/tests/lean/revert_frozen_dep.lean
new file mode 100644
index 0000000000..28fe85e04c
--- /dev/null
+++ b/tests/lean/revert_frozen_dep.lean
@@ -0,0 +1,4 @@
+lemma ex {α : id Type} [has_add α] : true :=
+begin
+  dsimp at α -- should fail because the frozen instance `[has_add α]` depends on `α`
+end
diff --git a/tests/lean/revert_frozen_dep.lean.expected.out b/tests/lean/revert_frozen_dep.lean.expected.out
new file mode 100644
index 0000000000..eab75a449f
--- /dev/null
+++ b/tests/lean/revert_frozen_dep.lean.expected.out
@@ -0,0 +1 @@
+revert_frozen_dep.lean:4:0: error: failed to revert '_inst_1', it is a frozen local instance (possible solution: use tactic `tactic.unfreeze_local_instances` to reset the set of local instances)