src/HOL/Code_Generator.thy
changeset 21079 747d716e98d0
parent 21059 361e62500ab7
child 21110 fc98cb66c5c3
--- 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 *}