diff -r 9b1b50514b5e -r b34c8aa657a5 src/HOL/eqrule_HOL_data.ML
--- a/src/HOL/eqrule_HOL_data.ML	Tue Jun 28 15:26:45 2005 +0200
+++ b/src/HOL/eqrule_HOL_data.ML	Tue Jun 28 15:27:45 2005 +0200
@@ -33,7 +33,7 @@
 val tranformation_pairs =
   [("op -->", [mp]), ("op &", [conjunct1,conjunct2]),
    ("All", [spec]), ("True", []), ("False", []),
-   ("If", [if_bool_eq_conj RS iffD1])];
+   ("HOL.If", [if_bool_eq_conj RS iffD1])];
 
 (*
 val mk_atomize:      (string * thm list) list -> thm -> thm list