1.1 --- a/src/HOL/List.thy	Tue Oct 07 16:07:18 2008 +0200
     1.2 +++ b/src/HOL/List.thy	Tue Oct 07 16:07:20 2008 +0200
     1.3 @@ -3661,7 +3661,7 @@
     1.4    member :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
     1.5  where 
     1.6    "x mem [] \<longleftrightarrow> False"
     1.7 -  | "x mem (y#ys) \<longleftrightarrow> (if y = x then True else x mem ys)"
     1.8 +  | "x mem (y#ys) \<longleftrightarrow> x = y \<or> x mem ys"
     1.9  
    1.10  primrec
    1.11    null:: "'a list \<Rightarrow> bool"