--- a/src/HOL/Wellfounded.thy Thu Mar 11 14:39:58 2010 +0100
+++ b/src/HOL/Wellfounded.thy Thu Mar 11 14:40:29 2010 +0100
@@ -8,7 +8,7 @@
header {*Well-founded Recursion*}
theory Wellfounded
-imports Transitive_Closure Big_Operators
+imports Transitive_Closure
uses ("Tools/Function/size.ML")
begin