diff -r f24fd4689d00 -r b1cd040ff5f7 IntEx.thy
--- a/IntEx.thy	Fri Nov 27 09:16:32 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 10:04:49 2009 +0100
@@ -142,7 +142,7 @@
 
 ML {*
 fun lift_tac_fset lthy t =
-  lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs
+  lift_tac lthy t [rel_eqv] rty [quot] rsp_thms defs
 *}
 
 lemma "PLUS a b = PLUS b a"
@@ -191,7 +191,7 @@
 lemma "PLUS (PLUS i j) k = PLUS i (PLUS j k)"
 apply(tactic {* procedure_tac @{context} @{thm plus_assoc_pre} 1 *})
 apply(tactic {* regularize_tac @{context} [rel_eqv] [rel_refl] 1 *})
-apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] trans2 rsp_thms) 1 *})
+apply(tactic {* REPEAT_ALL_NEW (r_mk_comb_tac @{context} rty [quot] [rel_refl] [trans2] rsp_thms) 1 *})
 oops