# HG changeset patch
# User wenzelm
# Date 1703931965 -3600
# Node ID bd52ab785b7b8ffff6dcc8df69d7a95267087893
# Parent  1488e69fd2a15850dbca557653b9844f0f07413e
minor performance tuning, following 703201dbd413;

diff -r 1488e69fd2a1 -r bd52ab785b7b src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 30 11:25:29 2023 +0100
+++ b/src/Pure/thm.ML	Sat Dec 30 11:26:05 2023 +0100
@@ -1063,8 +1063,10 @@
         fun lt (S1, S2) = le (S1, S2) andalso not (le (S2, S1));
         fun rel (S1, S2) = if S1 = S2 then [] else [(Term.aT S1, S2)];
 
-        val present =
-          (fold_terms {hyps = true} o fold_types o fold_atyps_sorts) (insert (eq_fst op =)) thm [];
+        val present_set =
+          Types.build (thm |> (fold_terms {hyps = true} o fold_types o fold_atyps) Types.add_set);
+        val present = map (fn T => (T, Type.sort_of_atyp T)) (Types.list_set present_set);
+
         val extra = fold (Sorts.remove_sort o #2) present shyps;
         val witnessed = Sign.witness_sorts thy present extra;
         val non_witnessed = fold (Sorts.remove_sort o #2) witnessed extra |> map (`minimize);