src/HOL/List.thy

   (Haskell infixl 4 "==")
 
 code_const "Code_Generator.eq \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
+code_reserved SML
+  list char
+
+code_reserved Haskell
+  Char
+
 setup {*
 let
 
 fun list_codegen thy defs gr dep thyname b t =
   let val (gr', ps) = foldl_map (Codegen.invoke_codegen thy defs dep thyname false)

 
 
 subsubsection {* Generation of efficient code *}
 
 consts
-  mem :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl 55)
+  memberl :: "'a \<Rightarrow> 'a list \<Rightarrow> bool" (infixl "mem" 55)
   null:: "'a list \<Rightarrow> bool"
   list_inter :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   list_ex :: "('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> bool"
   list_all :: "('a \<Rightarrow> bool) \<Rightarrow> ('a list \<Rightarrow> bool)"
   itrev :: "'a list \<Rightarrow> 'a list \<Rightarrow> 'a list"
   filtermap :: "('a \<Rightarrow> 'b option) \<Rightarrow> 'a list \<Rightarrow> 'b list"
   map_filter :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> 'a list \<Rightarrow> 'b list"
 
 primrec
   "x mem [] = False"
-  "x mem (y#ys) = (if y = x then True else x mem ys)"
+  "x mem (y#ys) = (x = y \<or> x mem ys)"
 
 primrec
   "null [] = True"
   "null (x#xs) = False"