# HG changeset patch
# User wenzelm
# Date 1729350976 -7200
# Node ID dff445a16252c22e2fb98257b642aa6d2f9326ad
# Parent  0123c6c8f38ab972831c477416843b1a1caf902f
more type information;

diff -r 0123c6c8f38a -r dff445a16252 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sat Oct 19 17:00:14 2024 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Sat Oct 19 17:16:16 2024 +0200
@@ -862,8 +862,8 @@
 
 (* type reflection *)
 
-fun type_tr' ctxt (Type ("itself", [T])) ts =
-      Term.list_comb (Syntax.const "_TYPE" $ term_of_typ ctxt T, ts)
+fun type_tr' ctxt (ty as Type ("itself", [T])) ts =
+      Term.list_comb (Const ("_TYPE", ty) $ term_of_typ ctxt T, ts)
   | type_tr' _ _ _ = raise Match;