# HG changeset patch
# User wenzelm
# Date 1728995797 -7200
# Node ID aaf9e7535a1a6d387cc06345bba3db0b132d3310
# Parent  26ecbac09941c4db9982fa274ae8300e18d1e7a8
revert redundant guard (T = dummyT) from 0278f6d87bad;

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