added reserved words for Haskell

--- a/src/HOL/Code_Generator.thy	Fri Oct 20 17:07:26 2006 +0200
+++ b/src/HOL/Code_Generator.thy	Fri Oct 20 17:07:27 2006 +0200
@@ -106,6 +106,8 @@
 code_const arbitrary
   (Haskell target_atom "(error \"arbitrary\")")
 
+code_reserved SML Fail
+code_reserved Haskell error
 
 subsection {* Operational equality for code generation *}
 
@@ -169,6 +171,8 @@
 code_const "eq \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
+code_reserved Haskell
+  Eq eq
 
 subsection {* normalization by evaluation *}
 

--- a/src/HOL/Datatype.thy	Fri Oct 20 17:07:26 2006 +0200
+++ b/src/HOL/Datatype.thy	Fri Oct 20 17:07:27 2006 +0200
@@ -807,6 +807,12 @@
 code_const "Code_Generator.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
   (Haskell infixl 4 "==")
 
+code_reserved SML
+  bool true false not unit option NONE SOME
+
+code_reserved Haskell
+  Bool True False not Maybe Nothing Just
+
 ML
 {*
 val apfst_conv = thm "apfst_conv";

--- a/src/HOL/Integ/IntDef.thy	Fri Oct 20 17:07:26 2006 +0200
+++ b/src/HOL/Integ/IntDef.thy	Fri Oct 20 17:07:27 2006 +0200
@@ -943,6 +943,9 @@
   (SML target_atom "IntInf.~")
   (Haskell target_atom "negate")
 
+code_reserved SML IntInf
+code_reserved Haskell Integer negate
+
 ML {*
 fun number_of_codegen thy defs gr dep module b (Const ("Numeral.number_of",
       Type ("fun", [_, T as Type ("IntDef.int", [])])) $ bin) =

--- a/src/HOL/Library/MLString.thy	Fri Oct 20 17:07:26 2006 +0200
+++ b/src/HOL/Library/MLString.thy	Fri Oct 20 17:07:27 2006 +0200
@@ -74,4 +74,7 @@
   (SML target_atom "String.explode")
   (Haskell "_")
 
+code_reserved SML string explode
+code_reserved Haskell string
+
 end

--- a/src/HOL/List.thy	Fri Oct 20 17:07:26 2006 +0200
+++ b/src/HOL/List.thy	Fri Oct 20 17:07:27 2006 +0200
@@ -2648,6 +2648,12 @@
 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
 
@@ -2682,7 +2688,7 @@
 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"
@@ -2693,7 +2699,7 @@
 
 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"

--- a/src/HOL/ex/CodeEmbed.thy	Fri Oct 20 17:07:26 2006 +0200
+++ b/src/HOL/ex/CodeEmbed.thy	Fri Oct 20 17:07:27 2006 +0200
@@ -85,4 +85,6 @@
   (SML "Term.Type (_, _)" and "Term.TFree (_, _)"
     and "Term.Const (_, _)" and "Term.$ (_, _)" and "Term.Free (_, _)")
 
+code_reserved SML Term
+
 end
\ No newline at end of file