Michael Norrish

If you want to add additional bindings so that theorems are available under two names, that's fine. On the other hand, don't _remove_ existing bindings to break stuff gratuitously. I'd...

I don't think context can be inferred because these functions can occur on the RHSes of arbitrary variable definitions which may then be used in different places.

Hmm. Good point. I think that in theory `make` is supposed to expand at time of use, but I'm not so sure Holmake does this.

Indeed.

I was actually thinking that it might be worthwhile to further *add* a location field. The parser could use these additional fields almost everywhere. Tactics that fail because a term...

For example, try ``` grep -r --include='*.sml' failwith.*term_to_string src ``` or ``` grep -r --include='*.sml' ERR.*term_to_string src ``` This will return a subset of the occurrences because it requires the...

This is a good idea, though I'd perhaps prefer to use the slight abstraction provided by our existing `UniversalType` to get the same effect. I'd keep the common cases of...

Absolutely!

One issue with this is that the `HOL_ERR` exception declaration has to happen in a context where terms and types are in scope. Currently, it’s declared *before* the kernel's types...

I think there are two failings: - the sharing is done for each theory independently. Which I guess is what you mean by *there's no attempt to handle cases where...