diff -r 508f3106b89c -r 2b7b349e470f QuotMain.thy
--- a/QuotMain.thy	Wed Dec 02 23:11:50 2009 +0100
+++ b/QuotMain.thy	Wed Dec 02 23:31:30 2009 +0100
@@ -990,7 +990,7 @@
 *}
 
 ML {*
-fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
+fun inj_repabs_tac ctxt quot_thms rel_refl trans2 =
   (FIRST' [
     (* "cong" rule of the of the relation / transitivity*)
     (* (op =) (R a b) (R c d) ----> \<lbrakk>R a c; R b d\<rbrakk> *)
@@ -1050,8 +1050,8 @@
 *}
 
 ML {*
-fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 =
-  REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2)
+fun all_inj_repabs_tac ctxt quot_thms rel_refl trans2 =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt quot_thms rel_refl trans2)
 *}
 
 section {* Cleaning of the theorem *}
@@ -1276,7 +1276,8 @@
 
 ML {*
 (* FIXME/TODO should only get as arguments the rthm like procedure_tac *)
-fun lift_tac lthy rthm rel_eqv rty quot defs =
+
+fun lift_tac lthy rthm rel_eqv quot defs =
   ObjectLogic.full_atomize_tac
   THEN' gen_frees_tac lthy
   THEN' Subgoal.FOCUS (fn {context, concl, ...} =>
@@ -1291,7 +1292,7 @@
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               rtac thm THEN' all_inj_repabs_tac lthy rty quot rel_refl trans2,
+               rtac thm THEN' all_inj_repabs_tac lthy quot rel_refl trans2,
                clean_tac lthy quot defs]]
     end) lthy
 *}