defncong adds cong twice

[xrchz]

This script file raises a Bind exception unexpectedly.

open HolKernel boolLib bossLib

val () = new_theory "bug";

Definition apply_def:
  apply f x = f x
End

val n1 = List.length $ DefnBase.read_congs();

Theorem apply_cong[defncong]:
  (!x. f x = f' x)
  ==>
  apply f = apply f'
Proof
  rw[apply_def, FUN_EQ_THM]
QED

val n2 = List.length $ DefnBase.read_congs();

val 1 = n2 - n1;

val () = export_theory();

[xrchz]

Using DefnBase.export_cong "apply_cong"; instead of [defncong] has the same problem. Using DefnBase.add_cong works.

[mn200]

Thanks for the report!

[ordinarymath]

Note that it only seems to appear for interactive mode. Building a theory and having it depend on bug with the check removed there's only one cong. I suspect that its this causing https://github.com/HOL-Theorem-Prover/HOL/blob/aa266667af464b9d3a22e8be1415d8f3af014c82/src/coretypes/DefnBase.sml#L166C1-L166C28

[mn200]

I doubt that's the issue; that entry-point is to support users removing things from theorem-sets. There's no way to access that functionality from the user-side of things with defncong (perhaps there should be, but that's another story), so having a null remove function should be fine.