--- 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})))*)
     ])
 *}