# HG changeset patch
# User wenzelm
# Date 1704840053 -3600
# Node ID 3d867a43041308b9b2039e14aba1d834c65adc4b
# Parent  f0fab78a418a4a5f9cfb12a52426041ad3287f3e
more robust: certify types uniformly (see also 62b75508eb66);

diff -r f0fab78a418a -r 3d867a430413 src/Pure/consts.ML
--- a/src/Pure/consts.ML	Tue Jan 09 23:38:54 2024 +0100
+++ b/src/Pure/consts.ML	Tue Jan 09 23:40:53 2024 +0100
@@ -198,6 +198,8 @@
                     else comb head
                 | _ => comb head)
             end
+        | Free (x, T) => comb (Free (x, expand_typ T))
+        | Var (xi, T) => comb (Var (xi, expand_typ T))
         | _ => comb head)
       end;
   in expand_term end;
@@ -303,7 +305,6 @@
       error ("Illegal schematic variables on rhs of abbreviation " ^ Binding.print b);
 
     val rhs = raw_rhs
-      |> Type.certify_types Type.mode_default tsig
       |> cert_term
       |> Term.close_schematic_term;
     val normal_rhs = expand_term rhs;