1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -55,12 +55,12 @@
     1.4    by (simp add: prod_fun_def split_def pdivmod_def nat_div_distrib nat_mod_distrib divmod_nat_div_mod)
     1.5  
     1.6  lemma eq_nat_code [code]:
     1.7 -  "eq_class.eq n m \<longleftrightarrow> eq_class.eq (of_nat n \<Colon> int) (of_nat m)"
     1.8 -  by (simp add: eq)
     1.9 +  "HOL.equal n m \<longleftrightarrow> HOL.equal (of_nat n \<Colon> int) (of_nat m)"
    1.10 +  by (simp add: equal)
    1.11  
    1.12  lemma eq_nat_refl [code nbe]:
    1.13 -  "eq_class.eq (n::nat) n \<longleftrightarrow> True"
    1.14 -  by (rule HOL.eq_refl)
    1.15 +  "HOL.equal (n::nat) n \<longleftrightarrow> True"
    1.16 +  by (rule equal_refl)
    1.17  
    1.18  lemma less_eq_nat_code [code]:
    1.19    "n \<le> m \<longleftrightarrow> (of_nat n \<Colon> int) \<le> of_nat m"
    1.20 @@ -332,7 +332,7 @@
    1.21    (Haskell "Nat.Nat")
    1.22    (Scala "Nat.Nat")
    1.23  
    1.24 -code_instance nat :: eq
    1.25 +code_instance nat :: equal
    1.26    (Haskell -)
    1.27  
    1.28  text {*
    1.29 @@ -442,7 +442,7 @@
    1.30    (Scala infixl 8 "/%")
    1.31    (Eval "Integer.div'_mod")
    1.32  
    1.33 -code_const "eq_class.eq \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
    1.34 +code_const "HOL.equal \<Colon> nat \<Rightarrow> nat \<Rightarrow> bool"
    1.35    (SML "!((_ : IntInf.int) = _)")
    1.36    (OCaml "Big'_int.eq'_big'_int")
    1.37    (Haskell infixl 4 "==")