diff -r 5c8cfaed32e6 -r 2b04504fcb69 src/HOL/Wellfounded.thy
--- a/src/HOL/Wellfounded.thy	Tue Jun 23 12:09:14 2009 +0200
+++ b/src/HOL/Wellfounded.thy	Tue Jun 23 12:09:30 2009 +0200
@@ -8,7 +8,7 @@
 
 theory Wellfounded
 imports Finite_Set Transitive_Closure
-uses ("Tools/function_package/size.ML")
+uses ("Tools/Function/size.ML")
 begin
 
 subsection {* Basic Definitions *}
@@ -693,7 +693,7 @@
 lemma in_inv_image[simp]: "((x,y) : inv_image r f) = ((f x, f y) : r)"
   by (auto simp:inv_image_def)
 
-text {* Measure functions into @{typ nat} *}
+text {* Measure Datatypes into @{typ nat} *}
 
 definition measure :: "('a => nat) => ('a * 'a)set"
 where "measure == inv_image less_than"
@@ -733,7 +733,7 @@
     "[| trans R1; trans R2 |] ==> trans (R1 <*lex*> R2)"
 by (unfold trans_def lex_prod_def, blast) 
 
-text {* lexicographic combinations with measure functions *}
+text {* lexicographic combinations with measure Datatypes *}
 
 definition 
   mlex_prod :: "('a \<Rightarrow> nat) \<Rightarrow> ('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set" (infixr "<*mlex*>" 80)
@@ -948,7 +948,7 @@
 
 subsection {* size of a datatype value *}
 
-use "Tools/function_package/size.ML"
+use "Tools/Function/size.ML"
 
 setup Size.setup