Stream: Isabelle/ML

Topic: simproc is not invoked in local theory during a proof in ML

Jason Hu (May 08 2026 at 18:50):

in a ML structure, I register a simproc using @{simproc_setup} antiquotation and I tested it fine in a HOL session. However, when I enter a proof context in ML, the simproc is not invoked at all from the trace log. here is what I have

  val enum_eq_simproc: simproc

and in the proof

simp_tac (context |> Config.put simp_trace true |> Config.put simp_trace_depth_limit 4 |> Simplifier.add_proc enum_eq_simproc) 1

You can see that I turned on the tracing flags, and then manually add the simproc to the simpset again. Isabelle issued a duplicated warning but still the simproc does not run on a matching pattern. what exactly is going wrong here?

Last updated: May 15 2026 at 17:41 UTC