diff -r 26ecbac09941 -r aaf9e7535a1a src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Tue Oct 15 14:19:58 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Tue Oct 15 14:36:37 2024 +0200
@@ -665,10 +665,8 @@
     val show_consts_markup = Config.get ctxt show_consts_markup;
 
     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;
+      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