--- 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")