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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
