--- a/src/HOL/Cardinals/Order_Union.thy	Wed Mar 05 18:28:57 2025 +0100
+++ b/src/HOL/Cardinals/Order_Union.thy	Tue Mar 11 10:20:44 2025 +0100
@@ -89,7 +89,7 @@
 
 lemma Osum_Preorder:
   "\<lbrakk>Field r Int Field r' = {}; Preorder r; Preorder r'\<rbrakk> \<Longrightarrow> Preorder (r Osum r')"
-  unfolding preorder_on_def using Osum_Refl Osum_trans by blast
+  unfolding preorder_on_def using Osum_Refl Osum_trans Restr_Field by blast
 
 lemma Osum_antisym:
   assumes FLD: "Field r Int Field r' = {}" and