src/HOL/Import/HOL/prob_extra.imp

   "EXP_DIV_TWO" > "HOL4Prob.prob_extra.EXP_DIV_TWO"
   "EXISTS_LONGEST" > "HOL4Prob.prob_extra.EXISTS_LONGEST"
   "EVEN_ODD_EXISTS_EQ" > "HOL4Prob.prob_extra.EVEN_ODD_EXISTS_EQ"
   "EVEN_ODD_BASIC" > "HOL4Prob.prob_extra.EVEN_ODD_BASIC"
   "EVEN_EXP_TWO" > "HOL4Prob.prob_extra.EVEN_EXP_TWO"
-  "EQ_EXT_EQ" > "Fun.ext_iff"
+  "EQ_EXT_EQ" > "Fun.fun_eq_iff"
   "DIV_TWO_UNIQUE" > "HOL4Prob.prob_extra.DIV_TWO_UNIQUE"
   "DIV_TWO_MONO_EVEN" > "HOL4Prob.prob_extra.DIV_TWO_MONO_EVEN"
   "DIV_TWO_MONO" > "HOL4Prob.prob_extra.DIV_TWO_MONO"
   "DIV_TWO_EXP" > "HOL4Prob.prob_extra.DIV_TWO_EXP"
   "DIV_TWO_CANCEL" > "HOL4Prob.prob_extra.DIV_TWO_CANCEL"