src/HOL/Fun.thy

--- a/src/HOL/Fun.thy	Mon Jan 10 22:03:24 2011 +0100
+++ b/src/HOL/Fun.thy	Tue Jan 11 14:12:37 2011 +0100
@@ -7,7 +7,7 @@
 
 theory Fun
 imports Complete_Lattice
-uses ("Tools/type_lifting.ML")
+uses ("Tools/enriched_type.ML")
 begin
 
 text{*As a simplification rule, it replaces all function equalities by
@@ -843,6 +843,6 @@
 
 subsubsection {* Functorial structure of types *}
 
-use "Tools/type_lifting.ML"
+use "Tools/enriched_type.ML"
 
 end