[isabelle-dev] record: fold_congs/unfold_congs

[Makarius]

This is probably mainly relevant to NICTA users of the record package.

When doing some cleanup and performance tuning of the record package, I 
discovered the following mysterious fold_congs and unfold_congs: 
http://isabelle.in.tum.de/repos/isabelle/file/d52da3e7aa4c/src/HOL/Tools/record.ML#l334

They appear to go back to the initial NICTA contribution 50406c4951d9. I 
have also seen traces of that feature in the L4.verified C parser tool 
that became publicly available recently.

Do these fold_congs/unfold_congs still have any purpose?  In the reachable 
set of Isabelle and AFP applications they don't, as far as I can see.  So 
it looks like a candidate for garbage collection on the sources.


 	Makarius