--- a/src/HOL/Product_Type.thy Fri Sep 10 09:56:28 2010 +0200
+++ b/src/HOL/Product_Type.thy Fri Sep 10 10:21:25 2010 +0200
@@ -29,7 +29,7 @@
by (simp_all add: equal)
code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
code_instance bool :: equal
(Haskell -)
@@ -110,7 +110,7 @@
(Haskell -)
code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
code_reserved SML
unit
@@ -281,7 +281,7 @@
(Haskell -)
code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
- (Haskell infixl 4 "==")
+ (Haskell infix 4 "==")
types_code
"prod" ("(_ */ _)")