diff -r 564ea783ace8 -r a010aab5bed0 src/HOL/Wellfounded.thy --- a/src/HOL/Wellfounded.thy Wed Jan 21 23:40:23 2009 +0100 +++ b/src/HOL/Wellfounded.thy Wed Jan 21 23:40:23 2009 +0100 @@ -7,7 +7,7 @@ header {*Well-founded Recursion*} theory Wellfounded -imports Finite_Set Nat +imports Finite_Set Transitive_Closure Nat uses ("Tools/function_package/size.ML") begin