diff -r 75af61f32ece -r f1c0a66284d3 QuotMain.thy
--- a/QuotMain.thy	Sat Nov 28 14:15:05 2009 +0100
+++ b/QuotMain.thy	Sat Nov 28 14:33:04 2009 +0100
@@ -878,7 +878,7 @@
 *}
 
 ML {*
-fun r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
+fun inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [resolve_tac trans2,
            lambda_res_tac ctxt,
            rtac @{thm RES_FORALL_RSP},
@@ -899,8 +899,8 @@
            weak_lambda_res_tac ctxt,
            CHANGED o (asm_full_simp_tac (HOL_ss addsimps @{thms FUN_REL_EQ}))])
 
-fun all_r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  REPEAT_ALL_NEW (r_mk_comb_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
+fun all_inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms =
+  REPEAT_ALL_NEW (inj_repabs_tac ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
 (*
@@ -927,7 +927,7 @@
 *)
 
 ML {*
-fun r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
+fun inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
   (FIRST' [
     (K (print_tac "start")) THEN' (K no_tac), 
   
@@ -990,8 +990,8 @@
 *}
 
 ML {*
-fun all_r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
-  REPEAT_ALL_NEW (r_mk_comb_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
+fun all_inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms =
+  REPEAT_ALL_NEW (inj_repabs_tac' ctxt rty quot_thms rel_refl trans2 rsp_thms)
 *}
 
 
@@ -1245,7 +1245,7 @@
        [rtac rule,
         RANGE [rtac rthm',
                regularize_tac lthy rel_eqv,
-               REPEAT_ALL_NEW (r_mk_comb_tac lthy rty quot rel_refl trans2 rsp_thms),
+               all_inj_repabs_tac lthy rty quot rel_refl trans2 rsp_thms,
                clean_tac lthy quot defs aps]]
     end) lthy
 *}