[isabelle-dev] Theory_Data.extend still needed?

Makarius makarius at sketis.net
Fri Jul 4 13:29:20 CEST 2014

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 

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.


More information about the isabelle-dev mailing list