--- a/src/HOL/HOL.thy Tue Nov 30 20:02:01 2010 -0800
+++ b/src/HOL/HOL.thy Wed Dec 01 11:33:17 2010 +0100
@@ -32,7 +32,7 @@
"Tools/async_manager.ML"
"Tools/try.ML"
("Tools/cnf_funcs.ML")
- ("Tools/functorial_mappers.ML")
+ ("Tools/type_mapper.ML")
begin
setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -712,7 +712,7 @@
and [Pure.elim?] = iffD1 iffD2 impE
use "Tools/hologic.ML"
-use "Tools/functorial_mappers.ML"
+use "Tools/type_mapper.ML"
subsubsection {* Atomizing meta-level connectives *}