Printing of dummy terms in syntax translations

[Makarius]

On 01/08/2026 15:32, Makarius wrote:
> 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.

I was delayed with many other things before Isabelle2026-RC1, so this was the 
first thing to inspect. It turned out that there are many more corner cases of 
printing abstractions: we have never taken it really serious in the past 3-4 
decades. I was tempted to improve on it, but that is very bad timing for the 
current release process. So I ended up mainly with this change:

changeset:   85671:fa5be76d009f
user:        wenzelm
date:        Mon Sep 21 19:38:30 2026 +0200
files:       NEWS src/Pure/Syntax/syntax_trans.ML 
src/Pure/type_infer_context.ML src/Pure/variable.ML
description:
more robust printing of terms with bound variables marked as "internal", e.g. 
from vacuous abstraction;

Thus all places where bound variables are printed --- via mark_bound_abs or 
mark_bound_body, to produce the "green" markup --- should give something that 
can be parsed again. The following examples produce a regular "uu" instead of 
internal "uu_":

   term "∀_∈A. b"
   term "λ(_, _). b"

In contrast, these guys produce an underscore, as before (because the print 
translation is different, but not 100% correct either):

   term "λ_. b"
   term "∀_. b"


> 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.
This has high priority, together with various improvements of many other 
binder-like print operations.

We shall also need explicit checks that printed output can be 
parsed/type-checked again: probably enabled by default, and disabled on request.


	Makarius