Cleaning up some obscure corners of the system, I've come across the old defer_recdef command. Are there any remaining uses of this historical relic? I don't see any in the main Isabelle repository + AFP. Makarius