diff -r 44045c743bfe -r 64c3c83e0ed4 QuotMain.thy
--- a/QuotMain.thy	Tue Nov 24 13:46:36 2009 +0100
+++ b/QuotMain.thy	Tue Nov 24 14:16:57 2009 +0100
@@ -691,6 +691,16 @@
 fun CHANGED' tac = (fn i => CHANGED (tac i))
 *}
 
+lemma prod_fun_id: "prod_fun id id \<equiv> id"
+by (rule eq_reflection) (simp add: prod_fun_def)
+
+lemma map_id: "map id \<equiv> id"
+apply (rule eq_reflection)
+apply (rule ext)
+apply (rule_tac list="x" in list.induct)
+apply (simp_all)
+done
+
 ML {*
 fun quotient_tac quot_thm =
   REPEAT_ALL_NEW (FIRST' [
@@ -699,9 +709,8 @@
     rtac @{thm IDENTITY_QUOTIENT},
     (* For functional identity quotients, (op = ---> op =) *)
     CHANGED' (
-      (simp_tac (HOL_ss addsimps @{thms FUN_MAP_I})) THEN'
-      rtac @{thm IDENTITY_QUOTIENT}
-    )
+      (simp_tac (HOL_ss addsimps @{thms eq_reflection[OF FUN_MAP_I] eq_reflection[OF id_apply] id_def_sym prod_fun_id map_id}
+      )))
   ])
 *}
 
@@ -808,15 +817,6 @@
 
 section {* Cleaning the goal *}
 
-lemma prod_fun_id: "prod_fun id id \<equiv> id"
-by (rule eq_reflection) (simp add: prod_fun_def)
-
-lemma map_id: "map id \<equiv> id"
-apply (rule eq_reflection)
-apply (rule ext)
-apply (rule_tac list="x" in list.induct)
-apply (simp_all)
-done
 
 ML {*
 fun simp_ids lthy thm =