# HG changeset patch
# User wenzelm
# Date 1704889108 -3600
# Node ID ec3dc36551ab0cddd586ad8edbe29f968b07251d
# Parent  4f862ca9a60a3dcf3ac5715efb26d56490e37b9b
tuned;

diff -r 4f862ca9a60a -r ec3dc36551ab src/Pure/consts.ML
--- a/src/Pure/consts.ML	Wed Jan 10 13:16:48 2024 +0100
+++ b/src/Pure/consts.ML	Wed Jan 10 13:18:28 2024 +0100
@@ -218,9 +218,9 @@
     fun term (Const (c, T)) =
           let
             val (T', same) = Same.commit_id typ T;
-            val decl = the_decl consts c;
+            val U = type_scheme consts c;
           in
-            if not (Type.raw_instance (T', #T decl)) then err_const (c, T)
+            if not (Type.raw_instance (T', U)) then err_const (c, T)
             else if same then raise Same.SAME else Const (c, T')
           end
       | term (Free (x, T)) = Free (x, typ T)