--- a/src/HOL/Datatype.thy Tue Sep 19 15:21:41 2006 +0200
+++ b/src/HOL/Datatype.thy Tue Sep 19 15:21:42 2006 +0200
@@ -9,6 +9,8 @@
imports Datatype_Universe
begin
+setup "DatatypeCodegen.setup2"
+
subsection {* Representing primitive types *}
rep_datatype bool
@@ -297,4 +299,10 @@
(SML target_atom "NONE" and target_atom "SOME")
(Haskell target_atom "Nothing" and target_atom "Just")
+code_instance option :: eq
+ (Haskell -)
+
+code_const "OperationalEquality.eq \<Colon> 'a\<Colon>eq option \<Rightarrow> 'a option \<Rightarrow> bool"
+ (Haskell infixl 4 "==")
+
end