[isabelle-dev] Global constant names in inductive

[Lars Hupel]

> Did you encounter an actual problem from that situation?
> 
> Formally, a comment is not a problem. "Fixing" such things prematurely
> is likely to break it.

Yes, there is an actual problem. I define a function via
"Function.add_function" and inspect the resulting info. As per usual
discipline this looks as follows:

val (info, (lthy', lthy)) = lthy'
  |> tap print_info
  |> Local_Theory.open_target |> snd
  |> Function.add_function bindings specs fun_config
       pat_completeness_auto
  |> (fn (info, lthy) => prove_termination lthy (#R info))
  ||> `Local_Theory.close_target

That is, I inspect the relation as generated by the function package.
The termination proof needs to get some information about that relation
from the inductive package. However, "#R" is a term, not a const name
string. Before I close the target, it will be a free variable.

With my change, I can lookup the inductive based on the term. Otherwise,
I'd need to construct the constant name and look it up using that.

Cheers
Lars