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