1.1 --- a/src/HOL/Code_Numeral.thy	Fri Sep 10 09:56:28 2010 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Fri Sep 10 10:21:25 2010 +0200
     1.3 @@ -345,7 +345,7 @@
     1.4  code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
     1.5    (SML "!((_ : Int.int) = _)")
     1.6    (OCaml "Big'_int.eq'_big'_int")
     1.7 -  (Haskell infixl 4 "==")
     1.8 +  (Haskell infix 4 "==")
     1.9    (Scala infixl 5 "==")
    1.10    (Eval "!((_ : int) = _)")
    1.11  

     2.1 --- a/src/HOL/HOL.thy	Fri Sep 10 09:56:28 2010 +0200
     2.2 +++ b/src/HOL/HOL.thy	Fri Sep 10 10:21:25 2010 +0200
     2.3 @@ -1942,10 +1942,10 @@
     2.4    (Haskell "Eq")
     2.5  
     2.6  code_const "HOL.equal"
     2.7 -  (Haskell infixl 4 "==")
     2.8 +  (Haskell infix 4 "==")
     2.9  
    2.10  code_const HOL.eq
    2.11 -  (Haskell infixl 4 "==")
    2.12 +  (Haskell infix 4 "==")
    2.13  
    2.14  text {* undefined *}
    2.15  

     3.1 --- a/src/HOL/Library/Code_Char.thy	Fri Sep 10 09:56:28 2010 +0200
     3.2 +++ b/src/HOL/Library/Code_Char.thy	Fri Sep 10 10:21:25 2010 +0200
     3.3 @@ -34,7 +34,7 @@
     3.4  code_const "HOL.equal \<Colon> char \<Rightarrow> char \<Rightarrow> bool"
     3.5    (SML "!((_ : char) = _)")
     3.6    (OCaml "!((_ : char) = _)")
     3.7 -  (Haskell infixl 4 "==")
     3.8 +  (Haskell infix 4 "==")
     3.9    (Scala infixl 5 "==")
    3.10  
    3.11  code_const "Code_Evaluation.term_of \<Colon> char \<Rightarrow> term"

     4.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Sep 10 09:56:28 2010 +0200
     4.2 +++ b/src/HOL/Library/Code_Integer.thy	Fri Sep 10 10:21:25 2010 +0200
     4.3 @@ -99,7 +99,7 @@
     4.4  code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
     4.5    (SML "!((_ : IntInf.int) = _)")
     4.6    (OCaml "Big'_int.eq'_big'_int")
     4.7 -  (Haskell infixl 4 "==")
     4.8 +  (Haskell infix 4 "==")
     4.9    (Scala infixl 5 "==")
    4.10    (Eval infixl 6 "=")
    4.11  

     5.1 --- a/src/HOL/Library/Code_Natural.thy	Fri Sep 10 09:56:28 2010 +0200
     5.2 +++ b/src/HOL/Library/Code_Natural.thy	Fri Sep 10 10:21:25 2010 +0200
     5.3 @@ -130,7 +130,7 @@
     5.4    (Scala infixl 8 "/%")
     5.5  
     5.6  code_const "HOL.equal \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"
     5.7 -  (Haskell infixl 4 "==")
     5.8 +  (Haskell infix 4 "==")
     5.9    (Scala infixl 5 "==")
    5.10  
    5.11  code_const "op \<le> \<Colon> code_numeral \<Rightarrow> code_numeral \<Rightarrow> bool"

     6.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Sep 10 09:56:28 2010 +0200
     6.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Sep 10 10:21:25 2010 +0200
     6.3 @@ -443,7 +443,7 @@
     6.4  code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
     6.5    (SML "!((_ : IntInf.int) = _)")
     6.6    (OCaml "Big'_int.eq'_big'_int")
     6.7 -  (Haskell infixl 4 "==")
     6.8 +  (Haskell infix 4 "==")
     6.9    (Scala infixl 5 "==")
    6.10    (Eval infixl 6 "=")
    6.11  

     7.1 --- a/src/HOL/List.thy	Fri Sep 10 09:56:28 2010 +0200
     7.2 +++ b/src/HOL/List.thy	Fri Sep 10 10:21:25 2010 +0200
     7.3 @@ -4829,7 +4829,7 @@
     7.4    (Haskell -)
     7.5  
     7.6  code_const "HOL.equal \<Colon> 'a list \<Rightarrow> 'a list \<Rightarrow> bool"
     7.7 -  (Haskell infixl 4 "==")
     7.8 +  (Haskell infix 4 "==")
     7.9  
    7.10  code_reserved SML
    7.11    list

     8.1 --- a/src/HOL/Option.thy	Fri Sep 10 09:56:28 2010 +0200
     8.2 +++ b/src/HOL/Option.thy	Fri Sep 10 10:21:25 2010 +0200
     8.3 @@ -128,7 +128,7 @@
     8.4    (Haskell -)
     8.5  
     8.6  code_const "HOL.equal \<Colon> 'a option \<Rightarrow> 'a option \<Rightarrow> bool"
     8.7 -  (Haskell infixl 4 "==")
     8.8 +  (Haskell infix 4 "==")
     8.9  
    8.10  code_reserved SML
    8.11    option NONE SOME

     9.1 --- a/src/HOL/Product_Type.thy	Fri Sep 10 09:56:28 2010 +0200
     9.2 +++ b/src/HOL/Product_Type.thy	Fri Sep 10 10:21:25 2010 +0200
     9.3 @@ -29,7 +29,7 @@
     9.4    by (simp_all add: equal)
     9.5  
     9.6  code_const "HOL.equal \<Colon> bool \<Rightarrow> bool \<Rightarrow> bool"
     9.7 -  (Haskell infixl 4 "==")
     9.8 +  (Haskell infix 4 "==")
     9.9  
    9.10  code_instance bool :: equal
    9.11    (Haskell -)
    9.12 @@ -110,7 +110,7 @@
    9.13    (Haskell -)
    9.14  
    9.15  code_const "HOL.equal \<Colon> unit \<Rightarrow> unit \<Rightarrow> bool"
    9.16 -  (Haskell infixl 4 "==")
    9.17 +  (Haskell infix 4 "==")
    9.18  
    9.19  code_reserved SML
    9.20    unit
    9.21 @@ -281,7 +281,7 @@
    9.22    (Haskell -)
    9.23  
    9.24  code_const "HOL.equal \<Colon> 'a \<times> 'b \<Rightarrow> 'a \<times> 'b \<Rightarrow> bool"
    9.25 -  (Haskell infixl 4 "==")
    9.26 +  (Haskell infix 4 "==")
    9.27  
    9.28  types_code
    9.29    "prod"     ("(_ */ _)")

    10.1 --- a/src/HOL/String.thy	Fri Sep 10 09:56:28 2010 +0200
    10.2 +++ b/src/HOL/String.thy	Fri Sep 10 10:21:25 2010 +0200
    10.3 @@ -207,7 +207,7 @@
    10.4  code_const "HOL.equal \<Colon> literal \<Rightarrow> literal \<Rightarrow> bool"
    10.5    (SML "!((_ : string) = _)")
    10.6    (OCaml "!((_ : string) = _)")
    10.7 -  (Haskell infixl 4 "==")
    10.8 +  (Haskell infix 4 "==")
    10.9    (Scala infixl 5 "==")
   10.10  
   10.11  types_code

    11.1 --- a/src/HOL/ex/Numeral.thy	Fri Sep 10 09:56:28 2010 +0200
    11.2 +++ b/src/HOL/ex/Numeral.thy	Fri Sep 10 10:21:25 2010 +0200
    11.3 @@ -1086,7 +1086,7 @@
    11.4  code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    11.5    (SML "!((_ : IntInf.int) = _)")
    11.6    (OCaml "Big'_int.eq'_big'_int")
    11.7 -  (Haskell infixl 4 "==")
    11.8 +  (Haskell infix 4 "==")
    11.9    (Scala infixl 5 "==")
   11.10    (Eval infixl 6 "=")
   11.11