diff -r 6b3be083229c -r b00a9b58264d QuotScript.thy
--- a/QuotScript.thy	Fri Dec 04 09:25:27 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 09:33:32 2009 +0100
@@ -137,7 +137,7 @@
 
 lemma FUN_REL_EQ:
   "(op =) ===> (op =) \<equiv> (op =)"
-by (simp add: expand_fun_eq)
+by (rule eq_reflection) (simp add: expand_fun_eq)
 
 lemma FUN_QUOTIENT:
   assumes q1: "QUOTIENT R1 abs1 rep1"