diff -r 258fa7b5a621 -r a74ea6d75571 src/HOL/Cardinals/Order_Union.thy
--- a/src/HOL/Cardinals/Order_Union.thy	Fri Jan 17 10:02:49 2014 +0100
+++ b/src/HOL/Cardinals/Order_Union.thy	Fri Jan 17 10:02:50 2014 +0100
@@ -7,7 +7,7 @@
 header {* Order Union *}
 
 theory Order_Union
-imports Wellfounded_More_FP
+imports Order_Relation
 begin
 
 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel"  (infix "Osum" 60) where