# HG changeset patch
# User wenzelm
# Date 1703969648 -3600
# Node ID d08460213400abf3ddbb00b5fc3e8d74fd96a469
# Parent  40e3d97b277ed4d0ab1a6580cea18683bfdebba0
tuned;

diff -r 40e3d97b277e -r d08460213400 src/Pure/thm.ML
--- a/src/Pure/thm.ML	Sat Dec 30 21:40:48 2023 +0100
+++ b/src/Pure/thm.ML	Sat Dec 30 21:54:08 2023 +0100
@@ -1076,12 +1076,15 @@
             if non_witnessed |> exists (fn (S', _) => lt (S', S)) then NONE else SOME S)
           |> Sorts.make;
 
-        val constrs' =
+        val non_witnessed_constraints =
           non_witnessed |> maps (fn (S1, S2) =>
             let val S0 = the (find_first (fn S => le (S, S1)) extra')
             in rel (S0, S1) @ rel (S1, S2) end);
 
-        val constraints' = fold (insert_constraints thy) (witnessed @ constrs') constraints;
+        val constraints' = constraints
+          |> fold (insert_constraints thy) witnessed
+          |> fold (insert_constraints thy) non_witnessed_constraints;
+
         val shyps' = fold (Sorts.insert_sort o #2) present extra';
 
         val replacements = present @ witnessed @ map (`Logic.dummy_tfree) extra';