src/HOL/HOL.thy

--- a/src/HOL/HOL.thy	Wed Nov 17 09:22:23 2010 +0100
+++ b/src/HOL/HOL.thy	Wed Nov 17 11:09:18 2010 +0100
@@ -32,6 +32,7 @@
   "Tools/async_manager.ML"
   "Tools/try.ML"
   ("Tools/cnf_funcs.ML")
+  ("Tools/functorial_mappers.ML")
 begin
 
 setup {* Intuitionistic.method_setup @{binding iprover} *}
@@ -708,6 +709,7 @@
   and [Pure.elim?] = iffD1 iffD2 impE
 
 use "Tools/hologic.ML"
+use "Tools/functorial_mappers.ML"
 
 
 subsubsection {* Atomizing meta-level connectives *}