# HG changeset patch
# User wenzelm
# Date 1703002042 -3600
# Node ID 6247ead9f5b0ec5ea89e027949c8319e27503709
# Parent  5c534c60e11e4f15ba8e458607d555eced7b4db6
tuned;

diff -r 5c534c60e11e -r 6247ead9f5b0 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Tue Dec 19 15:27:45 2023 +0100
+++ b/src/Pure/thm.ML	Tue Dec 19 17:07:22 2023 +0100
@@ -421,8 +421,9 @@
 fun insert_constraints_env thy env =
   let
     val tyenv = Envir.type_env env;
+    val normT = Envir.norm_type tyenv;
     fun insert ([], _) = I
-      | insert (S, T) = insert_constraints thy (Envir.norm_type tyenv T, S);
+      | insert (S, T) = insert_constraints thy (normT T, S);
   in tyenv |> Vartab.fold (insert o #2) end;
 
 end;