--- a/Quot/Examples/FSet.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/Examples/FSet.thy	Mon Dec 07 21:53:50 2009 +0100
@@ -303,7 +303,7 @@
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} [rel_refl] [trans2] 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} 1 *})
 apply(tactic {* clean_tac @{context} 1*})
 done
 
@@ -331,8 +331,6 @@
 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
-
 lemma "fmap f (FUNION (x::'b fset) (xa::'b fset)) = FUNION (fmap f x) (fmap f xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm map_append} 1 *})
 done
@@ -348,7 +346,7 @@
 apply(tactic {* regularize_tac @{context} 1 *})
 defer
 apply(tactic {* clean_tac @{context} 1 *})
-apply(tactic {* inj_repabs_tac_fset @{context} 1*})+
+apply(tactic {* inj_repabs_tac @{context} 1*})+
 done
 
 lemma list_induct_part:
@@ -390,10 +388,6 @@
 where
   "INSERT2 \<equiv> op #"
 
-ML {* val quot = @{thms Quotient_fset Quotient_fset2} *}
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t  *}
-
 lemma "P (x :: 'a fset2) (EMPTY :: 'c fset) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (INSERT e t)) \<Longrightarrow> P x l"
 apply (tactic {* lift_tac_fset @{context} @{thm list_induct_part} 1 *})
 done
@@ -425,9 +419,6 @@
   apply (auto)
   sorry
 
-ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t *}
-
 lemma "fset_rec (f1::'t) x (INSERT a xa) = x a xa (fset_rec f1 x xa)"
 apply (tactic {* lift_tac_fset @{context} @{thm list.recs(2)} 1 *})
 done

--- a/Quot/Examples/IntEx.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Mon Dec 07 21:53:50 2009 +0100
@@ -136,15 +136,6 @@
   shows "(intrel ===> intrel ===> intrel) my_plus my_plus"
 by (simp)
 
-ML {* val qty = @{typ "my_int"} *}
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
-
-ML {* fun lift_tac_intex lthy t = lift_tac lthy t *}
-
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [rel_refl] [trans2] *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [rel_refl] [trans2] *}
-
 lemma test1: "my_plus a b = my_plus a b"
 apply(rule refl)
 done
@@ -152,7 +143,7 @@
 lemma "PLUS a b = PLUS a b"
 apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *}) 
 done
 
@@ -162,13 +153,15 @@
 apply(rule refl)
 done
 
+
+
 lemma "PLUS a = PLUS a"
 apply(tactic {* procedure_tac @{context} @{thm test2} 1 *})
 apply(rule impI)
 apply(rule ballI)
 apply(rule apply_rsp[OF Quotient_my_int plus_rsp])
 apply(simp only: in_respects)
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -180,7 +173,7 @@
 apply(tactic {* procedure_tac @{context} @{thm test3} 1 *})
 apply(rule impI)
 apply(rule plus_rsp)
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -188,7 +181,7 @@
 lemma "PLUS a b = PLUS b a"
 apply(tactic {* procedure_tac @{context} @{thm plus_sym_pre} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -203,7 +196,7 @@
 lemma plus_assoc: "PLUS (PLUS x xa) xb = PLUS x (PLUS xa xb)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 done
 
@@ -214,7 +207,7 @@
 lemma "foldl PLUS x [] = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
@@ -225,7 +218,7 @@
 lemma "foldl PLUS x (h # t) = PLUS h (foldl PLUS x t)"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst2} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] cons_prs[OF Quotient_my_int])
 done
@@ -236,7 +229,7 @@
 lemma "foldl f (x::my_int) ([]::my_int list) = x"
 apply(tactic {* procedure_tac @{context} @{thm ho_tst3} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 (* TODO: does not work when this is added *)
 (* apply(tactic {* lambda_prs_tac @{context} 1 *})*)
 apply(tactic {* clean_tac @{context} 1 *})
@@ -249,7 +242,7 @@
 lemma "(\<lambda>x. (x, x)) (y::my_int) = (y, y)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp add: pair_prs)
 done
@@ -311,7 +304,7 @@
 lemma "(\<lambda>(y :: my_int). y) = (\<lambda>(x :: my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3a} 1 *})
 defer
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})
 apply(subst babs_rsp)
 apply(tactic {* clean_tac  @{context} 1 *})
@@ -329,7 +322,7 @@
 lemma "(\<lambda>(y :: my_int => my_int). y) = (\<lambda>(x :: my_int => my_int). x)"
 apply(tactic {* procedure_tac @{context} @{thm lam_tst3b} 1 *})
 defer
-apply(tactic {* all_inj_repabs_tac_intex @{context} 1*})
+apply(tactic {* all_inj_repabs_tac @{context} 1*})
 apply(tactic {* clean_tac  @{context} 1 *})
 apply(subst babs_rsp)
 apply(tactic {* clean_tac  @{context} 1 *})

--- a/Quot/Examples/IntEx2.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/Examples/IntEx2.thy	Mon Dec 07 21:53:50 2009 +0100
@@ -166,10 +166,6 @@
 text{*The integers form a @{text comm_ring_1}*}
 
 
-ML {* val qty = @{typ "int"} *}
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "int" *}
-
 instance int :: comm_ring_1
 proof
   fix i j k :: int

--- a/Quot/Examples/LFex.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/Examples/LFex.thy	Mon Dec 07 21:53:50 2009 +0100
@@ -218,12 +218,6 @@
 thm akind_aty_atrm.induct
 thm kind_ty_trm.induct
 
-ML {*
-  val quot = @{thms Quotient_KIND Quotient_TY Quotient_TRM}
-  val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) @{thms alpha_equivps}
-  val reps_same = map (fn x => @{thm Quotient_rel_rep} OF [x]) quot
-  val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quot
-*}
 
 lemma 
   assumes a0:
@@ -261,7 +255,7 @@
 apply - 
 apply(tactic {* procedure_tac @{context} @{thm akind_aty_atrm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} 1 *})
 apply(fold perm_kind_def perm_ty_def perm_trm_def)
 apply(tactic {* clean_tac @{context} 1 *})
 (*

--- a/Quot/Examples/LamEx.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/Examples/LamEx.thy	Mon Dec 07 21:53:50 2009 +0100
@@ -169,54 +169,48 @@
 apply (simp_all add: rlam.inject alpha_refl)
 done
 
-ML {* val qty = @{typ "lam"} *}
-ML {* val rsp_thms = @{thms perm_rsp fresh_rsp rVar_rsp rApp_rsp rLam_rsp rfv_rsp} *}
-
-ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
-ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "lam" *}
-ML {* fun lift_tac_lam lthy t = lift_tac lthy t *}
 
 lemma pi_var: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Var a = Var (pi \<bullet> a)"
-apply (tactic {* lift_tac_lam @{context} @{thm pi_var_com} 1 *})
+apply (tactic {* lift_tac @{context} @{thm pi_var_com} 1 *})
 done
 
 lemma pi_app: "(pi\<Colon>('x \<times> 'x) list) \<bullet> App (x\<Colon>lam) (xa\<Colon>lam) = App (pi \<bullet> x) (pi \<bullet> xa)"
-apply (tactic {* lift_tac_lam @{context} @{thm pi_app_com} 1 *})
+apply (tactic {* lift_tac @{context} @{thm pi_app_com} 1 *})
 done
 
 lemma pi_lam: "(pi\<Colon>('x \<times> 'x) list) \<bullet> Lam (a\<Colon>name) (x\<Colon>lam) = Lam (pi \<bullet> a) (pi \<bullet> x)"
-apply (tactic {* lift_tac_lam @{context} @{thm pi_lam_com} 1 *})
+apply (tactic {* lift_tac @{context} @{thm pi_lam_com} 1 *})
 done
 
 lemma fv_var: "fv (Var (a\<Colon>name)) = {a}"
-apply (tactic {* lift_tac_lam @{context} @{thm rfv_var} 1 *})
+apply (tactic {* lift_tac @{context} @{thm rfv_var} 1 *})
 done
 
 lemma fv_app: "fv (App (x\<Colon>lam) (xa\<Colon>lam)) = fv x \<union> fv xa"
-apply (tactic {* lift_tac_lam @{context} @{thm rfv_app} 1 *})
+apply (tactic {* lift_tac @{context} @{thm rfv_app} 1 *})
 done
 
 lemma fv_lam: "fv (Lam (a\<Colon>name) (x\<Colon>lam)) = fv x - {a}"
-apply (tactic {* lift_tac_lam @{context} @{thm rfv_lam} 1 *})
+apply (tactic {* lift_tac @{context} @{thm rfv_lam} 1 *})
 done
 
 lemma a1: "(a\<Colon>name) = (b\<Colon>name) \<Longrightarrow> Var a = Var b"
-apply (tactic {* lift_tac_lam @{context} @{thm a1} 1 *})
+apply (tactic {* lift_tac @{context} @{thm a1} 1 *})
 done
 
 lemma a2: "\<lbrakk>(x\<Colon>lam) = (xa\<Colon>lam); (xb\<Colon>lam) = (xc\<Colon>lam)\<rbrakk> \<Longrightarrow> App x xb = App xa xc"
-apply (tactic {* lift_tac_lam @{context} @{thm a2} 1 *})
+apply (tactic {* lift_tac @{context} @{thm a2} 1 *})
 done
 
 lemma a3: "\<lbrakk>(x\<Colon>lam) = [(a\<Colon>name, b\<Colon>name)] \<bullet> (xa\<Colon>lam); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> Lam a x = Lam b xa"
-apply (tactic {* lift_tac_lam @{context} @{thm a3} 1 *})
+apply (tactic {* lift_tac @{context} @{thm a3} 1 *})
 done
 
 lemma alpha_cases: "\<lbrakk>a1 = a2; \<And>a b. \<lbrakk>a1 = Var a; a2 = Var b; a = b\<rbrakk> \<Longrightarrow> P;
      \<And>x xa xb xc. \<lbrakk>a1 = App x xb; a2 = App xa xc; x = xa; xb = xc\<rbrakk> \<Longrightarrow> P;
      \<And>x a b xa. \<lbrakk>a1 = Lam a x; a2 = Lam b xa; x = [(a, b)] \<bullet> xa; a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> P\<rbrakk>
     \<Longrightarrow> P"
-apply (tactic {* lift_tac_lam @{context} @{thm alpha.cases} 1 *})
+apply (tactic {* lift_tac @{context} @{thm alpha.cases} 1 *})
 done
 
 lemma alpha_induct: "\<lbrakk>(qx\<Colon>lam) = (qxa\<Colon>lam); \<And>(a\<Colon>name) b\<Colon>name. a = b \<Longrightarrow> (qxb\<Colon>lam \<Rightarrow> lam \<Rightarrow> bool) (Var a) (Var b);
@@ -224,16 +218,16 @@
      \<And>(x\<Colon>lam) (a\<Colon>name) (b\<Colon>name) xa\<Colon>lam.
         \<lbrakk>x = [(a, b)] \<bullet> xa; qxb x ([(a, b)] \<bullet> xa); a \<notin> fv (Lam b x)\<rbrakk> \<Longrightarrow> qxb (Lam a x) (Lam b xa)\<rbrakk>
     \<Longrightarrow> qxb qx qxa"
-apply (tactic {* lift_tac_lam @{context} @{thm alpha.induct} 1 *})
+apply (tactic {* lift_tac @{context} @{thm alpha.induct} 1 *})
 done
 
 lemma var_inject: "(Var a = Var b) = (a = b)"
-apply (tactic {* lift_tac_lam @{context} @{thm rvar_inject} 1 *})
+apply (tactic {* lift_tac @{context} @{thm rvar_inject} 1 *})
 done
 
 lemma lam_induct:" \<lbrakk>\<And>name. P (Var name); \<And>lam1 lam2. \<lbrakk>P lam1; P lam2\<rbrakk> \<Longrightarrow> P (App lam1 lam2);
               \<And>name lam. P lam \<Longrightarrow> P (Lam name lam)\<rbrakk> \<Longrightarrow> P lam"
-apply (tactic {* lift_tac_lam @{context} @{thm rlam.induct} 1 *})
+apply (tactic {* lift_tac @{context} @{thm rlam.induct} 1 *})
 done
 
 lemma var_supp:

--- a/Quot/QuotMain.thy	Mon Dec 07 18:49:14 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 21:53:50 2009 +0100
@@ -186,6 +186,8 @@
 ML {*
 (* TODO/FIXME not needed anymore? *)
 fun SOLVES' tac = tac THEN_ALL_NEW (fn _ => no_tac)
+
+fun OF1 thm1 thm2 = thm2 RS thm1
 *}
 
 section {* atomize *}
@@ -292,36 +294,6 @@
    | _ => false
 *}
 
-section {* Infrastructure for collecting theorems for starting the lifting *}
-
-ML {*
-fun lookup_quot_data lthy qty =
-  let
-    val qty_name = fst (dest_Type qty)
-    val SOME quotdata = quotdata_lookup lthy qty_name
-    (* TODO: Should no longer be needed *)
-    val rty = Logic.unvarifyT (#rtyp quotdata)
-    val rel = #rel quotdata
-    val rel_eqv = #equiv_thm quotdata
-    val rel_refl = @{thm equivp_reflp} OF [rel_eqv]
-  in
-    (rty, rel, rel_refl, rel_eqv)
-  end
-*}
-
-ML {*
-fun lookup_quot_thms lthy qty_name =
-  let
-    val thy = ProofContext.theory_of lthy;
-    val trans2 = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".R_trans2")
-    val reps_same = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".REPS_same")
-    val absrep = PureThy.get_thm thy ("QUOT_TYPE_I_" ^ qty_name ^ ".thm10")
-    val quot = PureThy.get_thm thy ("Quotient_" ^ qty_name)
-  in
-    (trans2, reps_same, absrep, quot)
-  end
-*}
-
 section {* Regularization *} 
 
 (*
@@ -703,10 +675,12 @@
 
 ML {*
 fun solve_quotient_assums ctxt thm =
-  let val gl = hd (Drule.strip_imp_prems (cprop_of thm)) in
-  thm OF [Goal.prove_internal [] gl (fn _ => quotient_tac ctxt 1)]
-  end
-  handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
+let 
+  val goal = hd (Drule.strip_imp_prems (cprop_of thm)) 
+in
+  thm OF [Goal.prove_internal [] goal (fn _ => quotient_tac ctxt 1)]
+end
+handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
 *}
 
 (* Not used *)
@@ -914,9 +888,9 @@
 
     (* reflexivity of operators arising from Cong_tac *)
 | Const (@{const_name "op ="},_) $ _ $ _ 
-      => rtac @{thm refl} ORELSE'
+      => rtac @{thm refl} (*ORELSE'
           (resolve_tac trans2 THEN' RANGE [
-            quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])
+            quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)])*)
 
 (* TODO: These patterns should should be somehow combined and generalized... *)
 | (Const (@{const_name fun_rel}, _) $ _ $ _) $
@@ -943,29 +917,49 @@
 *}
 
 ML {*
-fun inj_repabs_tac ctxt rel_refl trans2 =
+fun inj_repabs_step_tac ctxt rel_refl trans2 =
   (FIRST' [
-    inj_repabs_tac_match ctxt trans2,
+    NDT ctxt "0" (inj_repabs_tac_match ctxt trans2),
     (* R (t $ \<dots>) (t' $ \<dots>) ----> apply_rsp   provided type of t needs lifting *)
+    
     NDT ctxt "A" (apply_rsp_tac ctxt THEN'
-                (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+                 RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)]),
+    
+    (* TODO/FIXME: I had to move this after the apply_rsp_tac - is this right *)
+    NDT ctxt "B" (resolve_tac trans2 THEN' 
+                 RANGE [quot_true_tac ctxt (fst o dest_bcomb), quot_true_tac ctxt (snd o dest_bcomb)]),
+
     (* (op =) (t $ \<dots>) (t' $ \<dots>) ----> Cong   provided type of t does not need lifting *)
     (* merge with previous tactic *)
-    NDT ctxt "B" (Cong_Tac.cong_tac @{thm cong} THEN'
+    NDT ctxt "C" (Cong_Tac.cong_tac @{thm cong} THEN'
                 (RANGE [quot_true_tac ctxt (fst o dest_comb), quot_true_tac ctxt (snd o dest_comb)])),
+    
     (* (op =) (\<lambda>x\<dots>) (\<lambda>x\<dots>) ----> (op =) (\<dots>) (\<dots>) *)
-    NDT ctxt "C" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+    NDT ctxt "D" (rtac @{thm ext} THEN' quot_true_tac ctxt unlam),
+    
     (* resolving with R x y assumptions *)
     NDT ctxt "E" (atac),
+    
     (* reflexivity of the basic relations *)
     (* R \<dots> \<dots> *)
-    NDT ctxt "D" (resolve_tac rel_refl)
+    NDT ctxt "F" (resolve_tac rel_refl)
     ])
 *}
 
 ML {*
-fun all_inj_repabs_tac ctxt rel_refl trans2 =
-  REPEAT_ALL_NEW (inj_repabs_tac ctxt rel_refl trans2)
+fun inj_repabs_tac ctxt =
+let
+  val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt)
+  val trans2 = map (fn x => @{thm equals_rsp} OF [x]) (quotient_rules_get ctxt)
+in
+  inj_repabs_step_tac ctxt rel_refl trans2
+end
+*}
+
+ML {*
+fun all_inj_repabs_tac ctxt =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt)
+(* if this is too slow we can inline the code above *)
 *}
 
 section {* Cleaning of the theorem *}
@@ -1190,24 +1184,19 @@
 *}
 
 ML {*
-(* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-
 fun lift_tac ctxt rthm =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac ctxt
-  THEN' CSUBGOAL (fn (gl, i) =>
+  THEN' CSUBGOAL (fn (goal, i) =>
     let
       val rthm' = atomize_thm rthm
-      val rule = procedure_inst ctxt (prop_of rthm') (term_of gl)
-      val rel_refl = map (fn x => @{thm equivp_reflp} OF [x]) (equiv_rules_get ctxt)
-      val quotients = quotient_rules_get ctxt
-      val trans2 = map (fn x => @{thm equals_rsp} OF [x]) quotients
-      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb gl))] @{thm QUOT_TRUE_i}
+      val rule = procedure_inst ctxt (prop_of rthm') (term_of goal)
+      val thm = Drule.instantiate' [] [SOME (snd (Thm.dest_comb goal))] @{thm QUOT_TRUE_i}
     in
       (rtac rule THEN'
        RANGE [rtac rthm',
               regularize_tac ctxt,
-              rtac thm THEN' all_inj_repabs_tac ctxt rel_refl trans2,
+              rtac thm THEN' all_inj_repabs_tac ctxt,
               clean_tac ctxt]) i
     end)
 *}