src/HOL/Import/HOL/bool.imp

--- a/src/HOL/Import/HOL/bool.imp	Mon Sep 06 22:58:06 2010 +0200
+++ b/src/HOL/Import/HOL/bool.imp	Tue Sep 07 10:05:19 2010 +0200
@@ -124,7 +124,7 @@
   "IMP_ANTISYM_AX" > "HOL4Setup.light_imp_as"
   "F_IMP" > "HOL4Base.bool.F_IMP"
   "F_DEF" > "HOL.False_def"
-  "FUN_EQ_THM" > "Fun.expand_fun_eq"
+  "FUN_EQ_THM" > "Fun.ext_iff"
   "FORALL_THM" > "HOL4Base.bool.FORALL_THM"
   "FORALL_SIMP" > "HOL.simp_thms_35"
   "FORALL_DEF" > "HOL.All_def"