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