diff --git a/iris/base_logic/lib/later_credits.v b/iris/base_logic/lib/later_credits.v
index 09b55d1c71ac84799ea45881aa2f3b5830ccb4ad..318fd089f8b318cac2c62a933811338ff365e521 100644
--- a/iris/base_logic/lib/later_credits.v
+++ b/iris/base_logic/lib/later_credits.v
@@ -40,7 +40,7 @@ Notation "'£'  n" := (lc n) (at level 1).
   Users should not directly interface with this. *)
 Local Definition lc_supply_def `{!lcGS Σ} (n : nat) : iProp Σ := own lcGS_name (● n).
 Local Definition lc_supply_aux : seal (@lc_supply_def). Proof. by eexists. Qed.
-Definition lc_supply := lc_supply_aux.(unseal).
+Local Definition lc_supply := lc_supply_aux.(unseal).
 Local Definition lc_supply_unseal :
   @lc_supply = @lc_supply_def := lc_supply_aux.(seal_eq).
 Global Arguments lc_supply {Σ _} n.