--- a/QuotList.thy	Fri Dec 04 09:10:31 2009 +0100
+++ b/QuotList.thy	Fri Dec 04 09:18:46 2009 +0100
@@ -15,7 +15,7 @@
 | "LIST_REL R (x#xs) (y#ys) = (R x y \<and> LIST_REL R xs ys)"
 
 lemma LIST_REL_EQ:
-  shows "LIST_REL (op =) = (op =)"
+  shows "LIST_REL (op =) \<equiv> (op =)"
 unfolding expand_fun_eq
 apply(rule allI)+
 apply(induct_tac x xa rule: list_induct2')

--- a/QuotMain.thy	Fri Dec 04 09:10:31 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 09:18:46 2009 +0100
@@ -956,7 +956,7 @@
 
     (* (op =) ===> (op =)  \<Longrightarrow> (op =), needed in order to apply respectfulness theorems *)
     (* global simplification *)
-    (*NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ] eq_reflection[OF LIST_REL_EQ]})))*)
+    (*NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*)
     ])
 *}
 

--- a/QuotScript.thy	Fri Dec 04 09:10:31 2009 +0100
+++ b/QuotScript.thy	Fri Dec 04 09:18:46 2009 +0100
@@ -136,7 +136,7 @@
   "E1 ===> E2 \<equiv> FUN_REL E1 E2"
 
 lemma FUN_REL_EQ:
-  "(op =) ===> (op =) = (op =)"
+  "(op =) ===> (op =) \<equiv> (op =)"
 by (simp add: expand_fun_eq)
 
 lemma FUN_QUOTIENT: