more robust (amending 1600fb749c54), to support the following corner case:
schematic_goal "PROP ((?f :: ?'a \<Rightarrow> _) (x :: ?'a))"
apply (tactic \<open>PRIMITIVE (Thm.instantiate (TVars.make1 ((("'a", 0), []), @{ctyp prop}), Vars.empty))\<close>)
oops

--- a/src/Pure/Isar/proof_display.ML	Sun Jan 28 19:22:33 2024 +0100
+++ b/src/Pure/Isar/proof_display.ML	Mon Jan 29 11:54:44 2024 +0100
@@ -280,7 +280,9 @@
           fun inst v =
             let
               val t = Var v;
-              val t' = Envir.subst_term (tyenv, tenv) (Envir.subst_term_types tyenv t);
+              val t' =
+                Envir.subst_term (tyenv, tenv) t handle TYPE _ =>
+                  Envir.subst_term (tyenv, tenv) (Envir.subst_term_types tyenv t);
             in if t aconv t' then NONE else SOME (prt_term t, prt_term t') end;
 
           fun inst_pair (x, y) = Pretty.item [x, Pretty.str " \<leadsto>", Pretty.brk 1, y];