--- a/IntEx.thy	Sat Nov 28 14:33:04 2009 +0100
+++ b/IntEx.thy	Sat Nov 28 14:45:22 2009 +0100
@@ -142,8 +142,7 @@
 
 ML {* fun lift_tac_intex lthy t = lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs *}
 
-
-ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac' lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
+ML {* fun inj_repabs_tac_intex lthy = inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}
 ML {* fun all_inj_repabs_tac_intex lthy = all_inj_repabs_tac lthy rty [quot] [rel_refl] [trans2] rsp_thms *}