src/HOL/HOL.thy

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