diff -r c3fbfd472365 -r f39f67982854 src/HOL/Map.ML
--- a/src/HOL/Map.ML	Fri Feb 07 16:40:23 2003 +0100
+++ b/src/HOL/Map.ML	Sat Feb 08 14:46:22 2003 +0100
@@ -221,7 +221,12 @@
 Goalw [dom_def] "a : dom m ==> ? b. m a = Some b";
 by Auto_tac;
 qed "domD";
-AddSDs [domD];
+
+Goalw [dom_def] "(a : dom m) = (m a ~= None)";
+by Auto_tac;
+qed "domIff";
+AddIffs [domIff];
+Delsimps [domIff];
 
 Goalw [dom_def] "dom empty = {}";
 by (Simp_tac 1);