src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Wed Mar 10 08:04:50 2010 +0100
+++ b/src/HOL/Wellfounded.thy	Wed Mar 10 16:53:27 2010 +0100
@@ -8,7 +8,7 @@
 header {*Well-founded Recursion*}
 
 theory Wellfounded
-imports Finite_Set Transitive_Closure
+imports Transitive_Closure Big_Operators
 uses ("Tools/Function/size.ML")
 begin