diff -r 020e27417b59 -r 0911d3aabf47 QuotMain.thy
--- a/QuotMain.thy	Mon Nov 30 12:14:20 2009 +0100
+++ b/QuotMain.thy	Mon Nov 30 15:32:14 2009 +0100
@@ -738,7 +738,7 @@
       end
   | _ =>
       (**************************************************)
-      (*  new
+      (*  new *)
       let
         val (rhead, rargs) = strip_comb rtrm
         val (qhead, qargs) = strip_comb qtrm
@@ -765,10 +765,10 @@
              list_comb (inj_repabs_trm lthy (rhead, qhead), rargs') 
         | _ => raise (LIFT_MATCH "injection")
       end
-      *)
+      (**)
 
       (*************************************************)
-      (* old *)
+      (* old
       let
         val (rhead, rargs) = strip_comb rtrm
         val (qhead, qargs) = strip_comb qtrm
@@ -792,7 +792,7 @@
                mk_repabs lthy (rty, qty) (list_comb (inj_repabs_trm lthy (rhead, qhead), rargs')) 
           | _ => raise (LIFT_MATCH "injection")
       end
-      (**)
+      *)
 end
 *}
 
@@ -1029,6 +1029,7 @@
 fun find_aps rtm qtm = distinct (op =) (find_aps_all rtm qtm)
 *}
 
+(* TODO: This is slow *)
 ML {*
 fun allex_prs_tac lthy quot =
   (EqSubst.eqsubst_tac lthy [0] @{thms all_prs ex_prs}) THEN' (quotient_tac quot)
@@ -1103,6 +1104,7 @@
 *}
 
 (*
+ TODO: Update
  Cleaning the theorem consists of 5 kinds of rewrites.
  These rewrites can be done independently and in any order.
 
@@ -1124,18 +1126,16 @@
 ML {*
 fun clean_tac lthy quot defs aps =
   let
-    val lower = flat (map (add_lower_defs lthy) defs)
-    val meta_lower = map (fn x => @{thm eq_reflection} OF [x]) lower
     val absrep = map (fn x => @{thm QUOTIENT_ABS_REP} OF [x]) quot
+    val meta_absrep = map (fn x => @{thm eq_reflection} OF [x]) absrep;
     val reps_same = map (fn x => @{thm QUOTIENT_REL_REP} OF [x]) quot
     val meta_reps_same = map (fn x => @{thm eq_reflection} OF [x]) reps_same
-    val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps (meta_reps_same @ meta_lower)
-    val aps_thms = map (applic_prs lthy absrep) aps
+    val simp_ctxt = (Simplifier.context lthy empty_ss) addsimps
+      (@{thm eq_reflection[OF fun_map.simps]} :: @{thms id_simps} @ meta_absrep @ meta_reps_same @ defs)
   in
     EVERY' [lambda_prs_tac lthy quot,
+            TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
             TRY o simp_tac simp_ctxt,
-            TRY o REPEAT_ALL_NEW (allex_prs_tac lthy quot),
-            TRY o REPEAT_ALL_NEW (EqSubst.eqsubst_tac lthy [0] aps_thms),
             TRY o rtac refl]
   end
 *}