# HG changeset patch
# User wenzelm
# Date 1728987482 -7200
# Node ID 0278f6d87bad67095e457316e3f835e8e4658f59
# Parent  aed72f8dc9c160ca71c3310237629361994b0394
tuned;

diff -r aed72f8dc9c1 -r 0278f6d87bad src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Mon Oct 14 19:48:59 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Oct 15 12:18:02 2024 +0200
@@ -658,13 +658,16 @@
 
 in
 
-fun term_to_ast ctxt trf tm =
+fun term_to_ast ctxt trf term =
   let
     val show_types = Config.get ctxt show_types orelse Config.get ctxt show_sorts;
     val show_markup = Config.get ctxt show_markup;
 
-    fun constrain_ast T ast =
-      Ast.Appl [Ast.Constant "_constrain", ast, ast_of_termT ctxt trf (term_of_typ ctxt T)];
+    fun constrain_ast clean T ast =
+      if T = dummyT then ast
+      else
+        let val U = Type_Annotation.print clean T
+        in Ast.Appl [Ast.Constant "_constrain", ast, ast_of_termT ctxt trf (term_of_typ ctxt U)] end;
 
     fun ast_of tm =
       (case strip_comb tm of
@@ -688,16 +691,11 @@
       handle Match => Ast.mk_appl (Ast.Constant a) (map ast_of args)
 
     and var_ast v T =
-      if (show_types orelse show_markup) andalso T <> dummyT then
-        let
-          val T' =
-            if show_markup andalso not show_types
-            then Type_Annotation.clean T
-            else Type_Annotation.smash T;
-        in simple_ast_of ctxt v |> constrain_ast T' end
-      else simple_ast_of ctxt v;
+      simple_ast_of ctxt v
+      |> (show_types orelse show_markup) ?
+          constrain_ast {clean = show_markup andalso not show_types} T;
   in
-    tm
+    term
     |> mark_aprop
     |> show_types ? prune_types
     |> Variable.revert_bounds ctxt
diff -r aed72f8dc9c1 -r 0278f6d87bad src/Pure/Syntax/type_annotation.ML
--- a/src/Pure/Syntax/type_annotation.ML	Mon Oct 14 19:48:59 2024 +0200
+++ b/src/Pure/Syntax/type_annotation.ML	Tue Oct 15 12:18:02 2024 +0200
@@ -12,6 +12,7 @@
   val is_omitted: typ -> bool
   val clean: typ -> typ
   val smash: typ -> typ
+  val print: {clean: bool} -> typ -> typ
   val fastype_of: typ list -> term -> typ
 end;
 
@@ -37,6 +38,9 @@
   | smash (Type (a, Ts)) = Type (a, map smash Ts)
   | smash T = T;
 
+fun print {clean = true} = clean
+  | print {clean = false} = smash;
+
 
 (* determine type -- propagate annotations *)