src/HOL/Wellfounded.thy

--- a/src/HOL/Wellfounded.thy	Wed Aug 22 22:47:16 2012 +0200
+++ b/src/HOL/Wellfounded.thy	Wed Aug 22 22:55:41 2012 +0200
@@ -9,7 +9,6 @@
 
 theory Wellfounded
 imports Transitive_Closure
-uses ("Tools/Function/size.ML")
 begin
 
 subsection {* Basic Definitions *}
@@ -845,8 +844,7 @@
 
 subsection {* size of a datatype value *}
 
-use "Tools/Function/size.ML"
-
+ML_file "Tools/Function/size.ML"
 setup Size.setup
 
 lemma size_bool [code]: