Ant S. (Jul 31 2026 at 20:48): Ant S. (Jul 31 2026 at 20:48):I am referring specifically to this library
I seem to end up with a compile-time error like this when using 2025-2 instead of 2025:
Binders FAILED (see also "isabelle build_log -H Error Binders")
...
*** (thm list list -> local_theory -> local_theory) * local_theory
*** Argument: (replicate (length specs) NONE) : 'a option list
*** Reason:
*** Can't unify context = Context.proof with 'a option list (*In Basis*)
*** (Different type constructors)
*** ML error (line 61 of "~/isa_pkgs/binder_datatypes/Tools/mrbnf_fp.ML"):
*** Type error in function application.
*** Function: ... ... true [] fixes specs' (replicate (length specs) NONE) :
Didn't want to cry wolf and post an issue on github before there is one, really.
Jan van Brügge (Jul 31 2026 at 21:39):this is weird, we test with 2025-2 in CI
Is this a recent clone?
Ant S. (Jul 31 2026 at 21:40):I just cloned this today
Last updated: Aug 05 2026 at 21:11 UTC