--- 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