From c76e44a6723afe4ea4ad2c3df7f5aa0888c5a9ce Mon Sep 17 00:00:00 2001
From: "F. G. Dorais" <fgdorais@gmail.com>
Date: Sun, 22 Dec 2024 05:38:52 -0500
Subject: [PATCH] fix: use throwUnknownConstant

---
 Batteries/Tactic/PrintOpaques.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Batteries/Tactic/PrintOpaques.lean b/Batteries/Tactic/PrintOpaques.lean
index 784ed5d031..2663421c7d 100644
--- a/Batteries/Tactic/PrintOpaques.lean
+++ b/Batteries/Tactic/PrintOpaques.lean
@@ -41,7 +41,7 @@ partial def collect (c : Name) : M Unit := do
       unless ← Meta.isProp v.type do
         modify fun s => { s with opaques := s.opaques.push c }
     | none                             =>
-      panic! s!"unknown constant {c}"
+      throwUnknownConstant c
 
 end CollectOpaques