[isabelle-dev] Remaining uses of defer_recdef?

[Makarius]

On Sat, 6 Jun 2015, Larry Paulson wrote:

> I’d be happy to see the complete phasing out of TFL. It’s had its day. 
> It was always a tricky thing to maintain. I’m amazed that it still works 
> despite all of the many fundamental changes to system APIs.

There are actually two remaining parts of TFL:

   (1) 'recdef' which is still used in Isabelle + AFP applications, but
     very rarely and some effort could be made to get rid of it.

   (2) 'defer_recdef' which is unused in the directly visible Isabelle
     universe.  So it could be deleted today.

This mailing list thread is an opportunity to point out dark matter in the 
Isabelle universe, where 'defer_recdef' still occurs.  Otherwise I will 
remove it soon, lets say within 1-2 weeks.


Apart from that we should also work on (1) eventually.  It has become a 
ritual to ask about the purpose of old 'recdef', and it usually leads to 
the result as "still needed" for odd reasons that I then forget 
immediately.  So I have developed a reluctance to ask again.


 	Makarius