diff -r 790310525e97 -r 8739f8abbecb src/HOL/Transfer.thy
--- a/src/HOL/Transfer.thy	Sat Mar 16 17:22:05 2013 +0100
+++ b/src/HOL/Transfer.thy	Sat Mar 16 20:51:23 2013 +0100
@@ -57,6 +57,9 @@
 definition is_equality :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool"
   where "is_equality R \<longleftrightarrow> R = (op =)"
 
+lemma is_equality_eq: "is_equality (op =)"
+  unfolding is_equality_def by simp
+
 text {* Handling of meta-logic connectives *}
 
 definition transfer_forall where
@@ -179,9 +182,6 @@
 
 subsection {* Properties of relators *}
 
-lemma is_equality_eq [transfer_rule]: "is_equality (op =)"
-  unfolding is_equality_def by simp
-
 lemma right_total_eq [transfer_rule]: "right_total (op =)"
   unfolding right_total_def by simp