Printing of dummy terms in syntax translations

[Lukas Stevens]

Dear Isabelle developers,

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. 
The algorithm places type annotations in terms such that printing and 
then parsing them again yields a term with the same type as the original 
term. This is crucial when trying to output well-formed Isar proofs.

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. You can observe this behavior in 
Isabelle/333ffbe82f5f, where

   term "λ_. 1 :: nat"

yields "λ_. 1" :: "'a ⇒ nat" while

   term "λ(x, _). 1 :: nat"

gives "λ(x, uu_). 1" :: "'a × 'b ⇒ nat", which contains an internal 
variable uu_. The latter term cannot be parsed after printing it due to 
the internal variable. Note that the same behavior surfaces for other 
users of Syntax_Trans.atomic_abs_tr' such as the translations for SOME 
and set comprehensions.

The reason for the first term being printed without internal variables 
is the changeset Isabelle/41986849fee0 that adds support for the syntax 
constant _idtdummy (printed as _) to Syntax_Trans.abs_tr'/mk_binder_tr'; 
however, case_prod_tr'/case_prod_guess_names_tr' internally uses 
Syntax_Trans.atomic_abs_tr', which has no support for _idtdummy. This 
could be changed by a 4-line modification of Syntax_Trans.atomic_abs_tr' 
(see attached diff), which produces the right result on the surface, 
although I am not sure if there is any collateral.

Anecdotally, I know that users of Sketch and Explore have stumbled over 
this behavior.

Cheers,

Lukas



-------------- next part --------------
diff -r 2300745395fc src/Pure/Syntax/syntax_trans.ML
--- a/src/Pure/Syntax/syntax_trans.ML	Wed Jul 01 12:27:01 2026 +0100
+++ b/src/Pure/Syntax/syntax_trans.ML	Tue Jul 07 11:43:26 2026 +0200
@@ -345,8 +345,11 @@
     (strip_abss ctxt strip_abs_vars strip_abs_body (eta_contr ctxt tm));
 
 fun atomic_abs_tr' ctxt (x, T, t) =
-  let val xT = singleton (variant_bounds ctxt t) (x, T)
-  in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
+  if Name.is_internal x andalso not (Term.is_dependent t) then
+    (Const ("_idtdummy", T), incr_boundvars ~1 t)
+  else
+    let val xT = singleton (variant_bounds ctxt t) (x, T)
+    in (mark_bound_abs xT, subst_bound (mark_bound_body xT, t)) end;
 
 fun abs_ast_tr' asts =
   (case Ast.unfold_ast_p "_abs" (Ast.Appl (Ast.Constant "_abs" :: asts)) of