# HG changeset patch
# User wenzelm
# Date 1706525684 -3600
#      Mon Jan 29 11:54:44 2024 +0100
# Node ID afa75b58166a37103e1263ad61ab13f51273a531
# Parent  24d6c4165b23b6acf60e31f5ff592626938258e3
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

diff -r 24d6c4165b23 -r afa75b58166a src/Pure/Isar/proof_display.ML
--- 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];