diff --git a/theories/logrel_heaplang/lib/symbol_adt.v b/theories/logrel_heaplang/lib/symbol_adt.v
index 1acc8070b1f6b66c14df63deb84a4f4f9f4942c0..fbbe57556bb34eea8359bb3455732ef9a9b97ffe 100644
--- a/theories/logrel_heaplang/lib/symbol_adt.v
+++ b/theories/logrel_heaplang/lib/symbol_adt.v
@@ -65,9 +65,6 @@ Section ltyped_symbol_adt.
   Definition symbol_inv (γ : gname) (l : loc) : iProp Σ :=
     (∃ n : nat, l ↦ #n ∗ counter γ n)%I.
 
-  Definition symbol_ctx (γ : gname) (l : loc) : iProp Σ :=
-    inv symbol_adtN (symbol_inv γ l).
-
   Definition lty_symbol (γ : gname) : lty Σ := Lty (λ w,
     ∃ n : nat, ⌜w = #n⌝ ∧ symbol γ n)%I.