more robust: certify types uniformly (see also 62b75508eb66);

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