Quoting Makarius :
It means that a "constant" c that depends on context parameters x y
z is turned into a fountational constant "loc.c" in the background,
and then re-imported into the local context as "loc.c x y z. Later
it might get re-interpreted such that its dependency on former
con
Hi Florian,
Anyway, I am not so much concerned about syntax. My primary intention
is to get rid of the experimental code in interpretation_with_defs.ML,
according to the following agenda:
a) Decide for a particular syntax (at the moment this can only be (*) as
it is conservative)
b) Enhance »in
