--- a/FSet.thy	Wed Dec 02 23:11:50 2009 +0100
+++ b/FSet.thy	Wed Dec 02 23:31:30 2009 +0100
@@ -300,12 +300,12 @@
 ML {* val (rty, rel, rel_refl, rel_eqv) = lookup_quot_data @{context} qty *}
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "fset"; *}
 ML {* val consts = lookup_quot_consts defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] [quot] defs *}
 
 lemma "IN x EMPTY = False"
 apply(tactic {* procedure_tac @{context} @{thm m1} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} rty [quot] [rel_refl] [trans2] 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} [quot] [rel_refl] [trans2] 1 *})
 apply(tactic {* clean_tac @{context} [quot] defs 1*})
 done
 
@@ -333,7 +333,7 @@
 apply(tactic {* lift_tac_fset @{context} @{thm fold1.simps(2)} 1 *})
 done
 
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy [quot] [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 *})
@@ -435,8 +435,8 @@
 
 ML {* val defs = @{thms EMPTY2_def INSERT2_def} @ defs *}
 ML {* val quot = @{thms QUOTIENT_fset QUOTIENT_fset2} *}
-ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy rty quot [rel_refl] [trans2] *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty quot defs *}
+ML {* fun inj_repabs_tac_fset lthy = inj_repabs_tac lthy quot [rel_refl] [trans2] *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot defs *}
 
 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 *})
@@ -471,7 +471,7 @@
 
 ML {* val rsp_thms = @{thms list_rec_rsp list_case_rsp} @ rsp_thms *}
 ML {* val defs = @{thms fset_rec_def fset_case_def} @ defs *}
-ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
+ML {* fun lift_tac_fset lthy t = lift_tac lthy t [rel_eqv] quot defs *}
 
 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 *})

--- a/IntEx.thy	Wed Dec 02 23:11:50 2009 +0100
+++ b/IntEx.thy	Wed Dec 02 23:31:30 2009 +0100
@@ -140,10 +140,10 @@
 ML {* val (trans2, reps_same, absrep, quot) = lookup_quot_thms @{context} "my_int"; *}
 ML {* val consts = lookup_quot_consts defs *}
 
-ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] defs *}
+ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] [quot] defs *}
 
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
-ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] *}
+ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
+ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy [quot] [rel_refl] [trans2] *}
 
 
 lemma "PLUS a b = PLUS b a"
@@ -252,7 +252,7 @@
 apply (rule allI)
 apply (rule allI)
 apply (rule impI)
-apply (induct_tac xb yb rule:list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
+apply (induct_tac xb yb rule: list_induct2) (* To finish I need to give it: arbitrary:xa ya *)
 sorry
 
 lemma nil_listrel_rsp[quot_rsp]:

--- a/LFex.thy	Wed Dec 02 23:11:50 2009 +0100
+++ b/LFex.thy	Wed Dec 02 23:31:30 2009 +0100
@@ -267,7 +267,7 @@
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
 prefer 2
 apply(tactic {* clean_tac @{context} quot defs 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2  1*})
+apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2  1*})
 done
 
 (* Does not work:
@@ -296,7 +296,7 @@
   \<Longrightarrow> P1 mkind \<and> P2 mty \<and> P3 mtrm"
 apply(tactic {* procedure_tac @{context} @{thm kind_ty_trm.induct} 1 *})
 apply(tactic {* regularize_tac @{context} @{thms alpha_EQUIVs} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} @{typ nat} quot rel_refl trans2 1 *})
+apply(tactic {* all_inj_repabs_tac @{context} quot rel_refl trans2 1 *})
 apply(tactic {* clean_tac @{context} quot defs 1 *})
 done
 

--- 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
 *}