src/HOL/HOL.thy
changeset 40858 69ab03d29c92
parent 40842 6c7d2a8761ed
parent 40855 149dcaa26728
child 40939 2c150063cd4d
     1.1 --- a/src/HOL/HOL.thy	Wed Dec 01 06:50:54 2010 -0800
     1.2 +++ b/src/HOL/HOL.thy	Wed Dec 01 18:00:40 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/functorial_mappers.ML")
     1.8 +  ("Tools/type_mapper.ML")
     1.9  begin
    1.10  
    1.11  setup {* Intuitionistic.method_setup @{binding iprover} *}
    1.12 @@ -712,7 +712,7 @@
    1.13    and [Pure.elim?] = iffD1 iffD2 impE
    1.14  
    1.15  use "Tools/hologic.ML"
    1.16 -use "Tools/functorial_mappers.ML"
    1.17 +use "Tools/type_mapper.ML"
    1.18  
    1.19  
    1.20  subsubsection {* Atomizing meta-level connectives *}