diff -r 8e736ce4c6f4 -r 78ece168f5b5 src/HOL/Library/Predicate_Compile_Alternative_Defs.thy
--- a/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Sun Sep 06 22:14:52 2015 +0200
+++ b/src/HOL/Library/Predicate_Compile_Alternative_Defs.thy	Wed Sep 09 17:07:44 2015 +0200
@@ -212,6 +212,18 @@
     done
 qed
 
+subsection \<open>Alternative rules for membership in lists\<close>
+
+declare in_set_member[code_pred_inline]
+
+lemma member_intros [code_pred_intro]:
+  "List.member (x#xs) x"
+  "List.member xs x \<Longrightarrow> List.member (y#xs) x"
+by(simp_all add: List.member_def)
+
+code_pred List.member
+  by(auto simp add: List.member_def elim: list.set_cases)
+
 section \<open>Setup for String.literal\<close>
 
 setup \<open>Predicate_Compile_Data.ignore_consts [@{const_name "STR"}]\<close>