--- a/QuotMain.thy	Fri Dec 04 08:19:56 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 09:10:31 2009 +0100
@@ -735,10 +735,8 @@
 ML {*
 fun quotient_tac ctxt =
   REPEAT_ALL_NEW (FIRST'
-    [resolve_tac (quotient_rules_get ctxt),
-     (* For functional identity quotients, (op = ---> op =) *)
-     (* TODO: think about the other way around, if we need to shorten the relation *)
-     CHANGED o (simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms id_simps}))])
+    [rtac @{thm IDENTITY_QUOTIENT},
+     resolve_tac (quotient_rules_get ctxt)])
 *}
 
 
@@ -954,11 +952,12 @@
     NDT ctxt "D" (resolve_tac rel_refl),
 
     (* resolving with R x y assumptions *)
-    NDT ctxt "E" (atac),
+    NDT ctxt "E" (atac)
 
     (* (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 eq_reflection[OF FUN_REL_EQ] eq_reflection[OF LIST_REL_EQ]})))*)
+    ])
 *}
 
 ML {*