# HG changeset patch
# User wenzelm
# Date 1662407945 -7200
# Node ID e39c1da9d904e6a7abd227d534e2fe3daeed9263
# Parent  0a6a138346da041c6dff79b5e49289934298c0a9
proper Envir.subst operations: env is already normalized, using Envir.norm may lead to non-termination;

diff -r 0a6a138346da -r e39c1da9d904 src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Mon Sep 05 21:20:38 2022 +0200
+++ b/src/Pure/Isar/proof_display.ML	Mon Sep 05 21:59:05 2022 +0200
@@ -258,19 +258,21 @@
       if Envir.is_empty env then []
       else
         let
+          val Envir.Envir {tyenv, tenv, ...} = env;
+
           val prt_type = Syntax.pretty_typ ctxt;
           val prt_term = Syntax.pretty_term ctxt;
 
           fun instT v =
             let
               val T = TVar v;
-              val T' = Envir.norm_type (Envir.type_env env) T;
+              val T' = Envir.subst_type tyenv T;
             in if T = T' then NONE else SOME (prt_type T, prt_type T') end;
 
           fun inst v =
             let
               val t = Var v;
-              val t' = Envir.norm_term env t;
+              val t' = Envir.subst_term (tyenv, tenv) 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];