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