1.1 --- a/src/HOL/HOL.thy	Sun Dec 05 14:02:16 2010 +0100
     1.2 +++ b/src/HOL/HOL.thy	Mon Dec 06 09:19:10 2010 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4    "Tools/async_manager.ML"
     1.5    "Tools/try.ML"
     1.6    ("Tools/cnf_funcs.ML")
     1.7 -  ("Tools/type_mapper.ML")
     1.8 +  ("Tools/type_lifting.ML")
     1.9    "~~/src/Tools/subtyping.ML"
    1.10  begin
    1.11  
    1.12 @@ -714,7 +714,7 @@
    1.13    and [Pure.elim?] = iffD1 iffD2 impE
    1.14  
    1.15  use "Tools/hologic.ML"
    1.16 -use "Tools/type_mapper.ML"
    1.17 +use "Tools/type_lifting.ML"
    1.18  
    1.19  
    1.20  subsubsection {* Atomizing meta-level connectives *}