tuned;

--- a/src/Pure/consts.ML	Tue Jan 09 23:52:02 2024 +0100
+++ b/src/Pure/consts.ML	Wed Jan 10 11:28:20 2024 +0100
@@ -186,8 +186,7 @@
         fun comb head' = Term.list_comb (head', args');
       in
         (case head of
-          Abs (x, T, t) => comb (Abs (x, expand_typ T, expand_term t))
-        | Const (c, T) =>
+          Const (c, T) =>
             let
               val T' = expand_typ T;
               val (_, ({T = U, ...}, abbr)) = the_entry consts c;
@@ -204,6 +203,7 @@
                     else comb head
                 | _ => comb head)
             end
+        | Abs (x, T, t) => comb (Abs (x, expand_typ T, expand_term t))
         | Free (x, T) => comb (Free (x, expand_typ T))
         | Var (xi, T) => comb (Var (xi, expand_typ T))
         | _ => comb head)