src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Sun Dec 05 14:02:16 2010 +0100
+++ b/src/HOL/HOL.thy	Mon Dec 06 09:19:10 2010 +0100
@@ -32,7 +32,7 @@
   "Tools/async_manager.ML"
   "Tools/try.ML"
   ("Tools/cnf_funcs.ML")
-  ("Tools/type_mapper.ML")
+  ("Tools/type_lifting.ML")
   "~~/src/Tools/subtyping.ML"
 begin
 
@@ -714,7 +714,7 @@
   and [Pure.elim?] = iffD1 iffD2 impE
 
 use "Tools/hologic.ML"
-use "Tools/type_mapper.ML"
+use "Tools/type_lifting.ML"
 
 
 subsubsection {* Atomizing meta-level connectives *}