diff -r 4562584d9d66 -r b8390cd56b8f src/HOL/Library/RType.thy
--- a/src/HOL/Library/RType.thy	Wed Sep 24 19:39:25 2008 +0200
+++ b/src/HOL/Library/RType.thy	Thu Sep 25 09:28:03 2008 +0200
@@ -91,9 +91,9 @@
 *}
 
 lemma [code func]:
-  "Typerep tyco1 tys1 = Typerep tyco2 tys2 \<longleftrightarrow> tyco1 = tyco2
-     \<and> list_all2 (op =) tys1 tys2"
-  by (auto simp add: list_all2_eq [symmetric])
+  "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])
 
 code_type typerep
   (SML "Term.typ")