--- a/IntEx.thy	Tue Nov 24 13:46:36 2009 +0100
+++ b/IntEx.thy	Tue Nov 24 14:16:57 2009 +0100
@@ -215,41 +215,53 @@
     end)
 *}
 
+ML {*
+val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} @{typ "my_int"}
+val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"
+*}
+
+(* FIXME: allex_prs and lambda_prs can be one function *)
+
+ML {*
+fun allex_prs_tac lthy quot =
+  (EqSubst.eqsubst_tac lthy [0] @{thms FORALL_PRS[symmetric] EXISTS_PRS[symmetric]})
+  THEN' (quotient_tac quot);
+*}
+
+ML {*
+fun lambda_prs_tac lthy quot =
+  (EqSubst.eqsubst_tac lthy [0] @{thms LAMBDA_PRS}
+  THEN' (RANGE [quotient_tac quot, quotient_tac quot]));
+*}
+
+ML {*
+fun clean_tac lthy quot defs reps_same =
+  let
+    val lower = flat (map (add_lower_defs lthy) defs)
+  in
+    (REPEAT_ALL_NEW (allex_prs_tac lthy quot)) THEN'
+    (REPEAT_ALL_NEW (lambda_prs_tac lthy quot)) THEN'
+    (REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] lower)) THEN'
+    (simp_tac (HOL_ss addsimps [reps_same]))
+  end
+*}
+
 lemma "\<forall>i j k. PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{thm plus_assoc_pre} @{context} 1 *})
-thm FORALL_PRS
-prefer 3
-(* phase 1 *)
-apply(subst FORALL_PRS[symmetric])
-apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-apply(subst FORALL_PRS[symmetric])
-apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-apply(subst FORALL_PRS[symmetric])
-apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-apply(subst LAMBDA_PRS)
-apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-apply(fold id_def)
-apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-apply(subst LAMBDA_PRS)
-apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-apply(fold id_def)
-apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-apply(subst LAMBDA_PRS)
-apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
-apply(fold id_def)
-apply(tactic {* quotient_tac @{thm QUOTIENT_my_int} 1 *})
+apply(tactic {* regularize_tac @{context} rel_eqv rel_refl 1 *})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty quot rel_refl trans2 rsp_thms) 1 *})
+apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *})
+done 
+
+apply(tactic {* REPEAT_ALL_NEW (allex_prs_tac @{context} quot) 1 *})
+apply(tactic {* REPEAT_ALL_NEW (lambda_prs_tac @{context} quot) 1 *})
 (* phase 2 *)
 ML_prf {*
  val lower = add_lower_defs @{context} @{thm PLUS_def}
 *}
-apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*})
-apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*})
-apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*})
-apply(tactic {* EqSubst.eqsubst_tac @{context} [0] lower 1*})
-(* phase 3 *)
-apply(subst QUOT_TYPE_I_my_int.REPS_same)
-apply(rule refl)
-
+apply(tactic {* REPEAT_ALL_NEW (EqSubst.eqsubst_tac @{context} [0] lower) 1*})
+apply(tactic {* simp_tac (HOL_ss addsimps [reps_same]) 1 *})
+done
 
 
 

--- 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 =