1.1 --- a/src/HOL/Code_Evaluation.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Code_Evaluation.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -162,7 +162,7 @@
     1.4  subsubsection {* Code generator setup *}
     1.5  
     1.6  lemmas [code del] = term.recs term.cases term.size
     1.7 -lemma [code, code del]: "eq_class.eq (t1\<Colon>term) t2 \<longleftrightarrow> eq_class.eq t1 t2" ..
     1.8 +lemma [code, code del]: "HOL.equal (t1\<Colon>term) t2 \<longleftrightarrow> HOL.equal t1 t2" ..
     1.9  
    1.10  lemma [code, code del]: "(term_of \<Colon> typerep \<Rightarrow> term) = term_of" ..
    1.11  lemma [code, code del]: "(term_of \<Colon> term \<Rightarrow> term) = term_of" ..