--- a/src/HOL/HOL.ML	Wed Jan 31 14:03:31 2007 +0100
+++ b/src/HOL/HOL.ML	Wed Jan 31 16:05:10 2007 +0100
@@ -14,7 +14,6 @@
 val cong = thm "cong"
 val conj_comms = thms "conj_comms";
 val conj_cong = thm "conj_cong";
-val def_imp_eq = thm "def_imp_eq";
 val de_Morgan_conj = thm "de_Morgan_conj";
 val de_Morgan_disj = thm "de_Morgan_disj";
 val disj_assoc = thm "disj_assoc";