src/HOL/Set.thy

 subsubsection {* Primitive predicates *}
 
 definition
   is_empty :: "'a set \<Rightarrow> bool"
 where
-  [code func del]: "is_empty A \<longleftrightarrow> A = {}"
+  [code func del, code post]: "is_empty A \<longleftrightarrow> A = {}"
 lemmas [code inline] = is_empty_def [symmetric]
 
 lemma is_empty_insert [code func]:
   "is_empty (insert a A) \<longleftrightarrow> False"
   by (simp add: is_empty_def)