1.1 --- a/src/HOL/Library/Code_Integer.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Library/Code_Integer.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    (Scala "BigInt")
     1.5    (Eval "int")
     1.6  
     1.7 -code_instance int :: eq
     1.8 +code_instance int :: equal
     1.9    (Haskell -)
    1.10  
    1.11  setup {*
    1.12 @@ -96,7 +96,7 @@
    1.13    (Scala "!((k: BigInt) => (l: BigInt) =>/ if (l == 0)/ (BigInt(0), k) else/ (k.abs '/% l.abs))")
    1.14    (Eval "Integer.div'_mod/ (abs _)/ (abs _)")
    1.15  
    1.16 -code_const "eq_class.eq \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    1.17 +code_const "HOL.equal \<Colon> int \<Rightarrow> int \<Rightarrow> bool"
    1.18    (SML "!((_ : IntInf.int) = _)")
    1.19    (OCaml "Big'_int.eq'_big'_int")
    1.20    (Haskell infixl 4 "==")