src/HOL/Library/Order_Union.thy

--- a/src/HOL/Library/Order_Union.thy	Mon Nov 18 18:04:44 2013 +0100
+++ b/src/HOL/Library/Order_Union.thy	Mon Nov 18 18:04:44 2013 +0100
@@ -7,7 +7,7 @@
 header {* Order Union *}
 
 theory Order_Union
-imports "~~/src/HOL/Cardinals/Wellfounded_More_Base" 
+imports "~~/src/HOL/Cardinals/Wellfounded_More_LFP" 
 begin
 
 definition Osum :: "'a rel \<Rightarrow> 'a rel \<Rightarrow> 'a rel"  (infix "Osum" 60) where