Printing of dummy terms in syntax translations

[Makarius]

On 07/07/2026 13:09, Lukas Stevens wrote:
> 
> I am working on the type annotation algorithm in ~~/src/HOL/Tools/ 
> Sledgehammer/sledgehammer_isar_annotate.ML that is used by some interactive 
> tools, e.g., Sledgehammer and Sketch and Explore.
> 
> While testing the algorithm, I ran into some unfortunate behavior that results 
> from the interaction of Syntax_Trans.atomic_abs_tr' and the syntax translation 
> case_prod_tr'/case_prod_guess_names_tr' in Product_Type.thy.
This is still open. I will take a brief look before we head to the 
Isabelle2026 release, to see if it is to be addressed before or after the release.

After the release I would like to absorb all previous attempts to print terms 
for re-parsing into Isabelle/Pure, such that becomes part of the regular 
functionality.


	Makarius