[isabelle-dev] adhoc overloading

[Christian Sternagel]

Dear all,

I'm currently (as of changeset e6433b34364b) investigating whether it 
would be possible to allow adhoc overloading (implemented in 
~~/src/Tools/adhoc_overloading.ML) inside local contexts.

Since I'm not too sure about the internals of local contexts, would that 
make sense in principle?

A related question: what is the difference between 
Syntax_Phases.term_check and Syntax_Phases.term_check'? Why does the 
latter expect a function returning an option but not the former?

And another one: assume we could do

   consts FOO :: ... (<some syntax>)
   setup {* Adhoc_Overloading.add_overloaded @{const_name FOO} *}

   locale foo =
     fixes foo :: ...
     assumes ...
   begin

   local_setup {*
     Adhoc_Overloading.add_variant @{const_name FOO} @{const_name foo}
   *}

would the overloading only be active inside foo or would it also have 
effects outside of this context (that are impossible to avoid due to 
technical reasons)? Does it make sense at all to use the locally fixed 
foo as a constant in the call to add_overloaded?

cheers

chris