[isabelle-dev] Theory_Data.extend still needed?

[Makarius]

On Sat, 28 Jun 2014, Florian Haftmann wrote:

> grep -rIPn 'val\s+extend\s*=\s*[^I ]' src
> ./Pure/context.ML:554:    val extend = Data.extend;
> 	(which is not relevant since this is the definition of Theory_Data istelf)

There are a few occurences of "fun extend", e.g. in src/Pure/theory.ML.
(Note that the "val" for extend or merge is a canonical source of SML/NJ 
unhappiness.)

Conceptually, the extend operation is a single-armed merge; the 
"implementation" manual also covers it to some extent. It allows data 
slots to participate in the graph structure (although there might be other 
ways to achieve that today, e.g. via theory begin/end hooks).

Actual use of extend is rare and usually somewhat exotic, but also happens 
to be in important kernel modules.  Since there is no true 
counterindication against it, we should keep things as is.


 	Makarius