diff -r 168dba35ecf3 -r 97775f3e8722 src/HOL/Typerep.thy
--- a/src/HOL/Typerep.thy	Fri Aug 27 15:36:02 2010 +0200
+++ b/src/HOL/Typerep.thy	Fri Aug 27 19:34:23 2010 +0200
@@ -78,9 +78,13 @@
 *}
 
 lemma [code]:
-  "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
-     \<and> list_all2 eq_class.eq tys1 tys2"
-  by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
+  "HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2
+     \<and> list_all2 HOL.equal tys1 tys2"
+  by (auto simp add: eq_equal [symmetric] list_all2_eq [symmetric])
+
+lemma [code nbe]:
+  "HOL.equal (x :: typerep) x \<longleftrightarrow> True"
+  by (fact equal_refl)
 
 code_type typerep
   (Eval "Term.typ")