src/HOL/Cardinals/Order_Union.thy

--- a/src/HOL/Cardinals/Order_Union.thy	Sat Nov 04 18:57:49 2017 +0100
+++ b/src/HOL/Cardinals/Order_Union.thy	Sat Nov 04 19:17:19 2017 +0100
@@ -7,7 +7,7 @@
 section \<open>Order Union\<close>
 
 theory Order_Union
-imports HOL.Order_Relation
+imports Main
 begin
 
 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel"  (infix "Osum" 60) where