# HG changeset patch
# User wenzelm
# Date 1662543814 -7200
# Node ID 1600fb749c54b0c9a146d51ad66a4653a4e5eba4
# Parent  0f48e873e187d98d488d3dfd066948f36f62b3e7
more robust: capture corner case seen in line 631 of "$AFP/Automatic_Refinement/Autoref_Bindings_HOL.thy" (AFP/6c87f24bb773);

diff -r 0f48e873e187 -r 1600fb749c54 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Wed Sep 07 11:25:49 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Wed Sep 07 11:43:34 2022 +0200
@@ -272,7 +272,7 @@
           fun inst v =
             let
               val t = Var v;
-              val t' = Envir.subst_term (tyenv, tenv) t;
+              val t' = 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 prt_eq (x, y) = Pretty.block [x, Pretty.str " =", Pretty.brk 1, y];