1.1 --- a/src/HOL/Typerep.thy	Fri Aug 27 15:36:02 2010 +0200
     1.2 +++ b/src/HOL/Typerep.thy	Fri Aug 27 19:34:23 2010 +0200
     1.3 @@ -78,9 +78,13 @@
     1.4  *}
     1.5  
     1.6  lemma [code]:
     1.7 -  "eq_class.eq (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> eq_class.eq tyco1 tyco2
     1.8 -     \<and> list_all2 eq_class.eq tys1 tys2"
     1.9 -  by (auto simp add: equals_eq [symmetric] list_all2_eq [symmetric])
    1.10 +  "HOL.equal (Typerep tyco1 tys1) (Typerep tyco2 tys2) \<longleftrightarrow> HOL.equal tyco1 tyco2
    1.11 +     \<and> list_all2 HOL.equal tys1 tys2"
    1.12 +  by (auto simp add: eq_equal [symmetric] list_all2_eq [symmetric])
    1.13 +
    1.14 +lemma [code nbe]:
    1.15 +  "HOL.equal (x :: typerep) x \<longleftrightarrow> True"
    1.16 +  by (fact equal_refl)
    1.17  
    1.18  code_type typerep
    1.19    (Eval "Term.typ")