executable domain membership checks

--- a/src/HOL/Map.thy	Mon Jun 05 20:03:01 2017 +0200
+++ b/src/HOL/Map.thy	Mon Jun 05 15:59:41 2017 +0200
@@ -485,7 +485,7 @@
 lemma domD: "a \<in> dom m \<Longrightarrow> \<exists>b. m a = Some b"
   by (cases "m a") (auto simp add: dom_def)
 
-lemma domIff [iff, simp del]: "a \<in> dom m \<longleftrightarrow> m a \<noteq> None"
+lemma domIff [iff, simp del, code_unfold]: "a \<in> dom m \<longleftrightarrow> m a \<noteq> None"
   by (simp add: dom_def)
 
 lemma dom_empty [simp]: "dom empty = {}"