[isabelle-dev] Remaining uses of defer_recdef?

[Makarius]

On Thu, 11 Jun 2015, Larry Paulson wrote:

> We must go forward and not back.

Just to conclude the original question on this thread: 'defer_recdef' is 
unused, untested, unmaintained.  So it falls under the normal 
garbage-collection of source code.  I will remove it next week or so, 
unless there is another strong argument to keep it.

In contrast, the main 'recdef' is maintained a bit longer; of course 
without any plans to "localize" it.  Asymptotically, 'function' should 
take over its role, but there is presently no attempt to change the 
situation.


 	Makarius