diff -r 6b3be083229c -r b00a9b58264d QuotMain.thy
--- a/QuotMain.thy	Fri Dec 04 09:25:27 2009 +0100
+++ b/QuotMain.thy	Fri Dec 04 09:33:32 2009 +0100
@@ -967,7 +967,7 @@
 (* A faster version *)
 
 ML {*
-fun inj_repabs_tac_fast ctxt quot_thms trans2 = SUBGOAL (fn (goal, i) =>
+fun inj_repabs_tac_fast ctxt trans2 = SUBGOAL (fn (goal, i) =>
 (case HOLogic.dest_Trueprop (Logic.strip_assums_concl goal) of
   ((Const (@{const_name FUN_REL}, _) $ _ $ _) $ (Abs _) $ (Abs _))
       => rtac @{thm FUN_REL_I} THEN' quot_true_tac ctxt unlam
@@ -992,29 +992,30 @@
     (resolve_tac trans2 THEN' RANGE [
       quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
 | _ $ _ $ _ =>
-    instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt quot_thms)]
+    instantiate_tac @{thm REP_ABS_RSP} ctxt THEN' RANGE [SOLVES' (quotient_tac ctxt)]
 ) i)
 *}
 
 ML {*
-fun inj_repabs_tac' ctxt quot_thms rel_refl trans2 =
+fun inj_repabs_tac' ctxt rel_refl trans2 =
   (FIRST' [
-    inj_repabs_tac_fast ctxt quot_thms trans2,
+    inj_repabs_tac_fast ctxt trans2,
     NDT ctxt "A" (APPLY_RSP_TAC ctxt THEN'
-                (RANGE [SOLVES' (quotient_tac ctxt quot_thms), SOLVES' (quotient_tac ctxt quot_thms),
+                (RANGE [SOLVES' (quotient_tac ctxt), SOLVES' (quotient_tac ctxt),
                         quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
     NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
     NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
     NDT ctxt "E" (atac),
     NDT ctxt "D" (resolve_tac rel_refl),
-    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt)),
-    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms eq_reflection[OF FUN_REL_EQ]})))])
+    NDT ctxt "7" (resolve_tac (rsp_rules_get ctxt))
+(*    NDT ctxt "H" (CHANGED o (asm_full_simp_tac ((Simplifier.context ctxt empty_ss) addsimps @{thms FUN_REL_EQ LIST_REL_EQ})))*)
+    ])
 *}
 
 ML {*
-fun all_inj_repabs_tac' ctxt quot_thms rel_refl trans2 =
-  REPEAT_ALL_NEW (inj_repabs_tac' ctxt quot_thms rel_refl trans2)
+fun all_inj_repabs_tac' ctxt rel_refl trans2 =
+  REPEAT_ALL_NEW (inj_repabs_tac' ctxt rel_refl trans2)
 *}