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