diff -r 5a9bdf81672d -r 3f3927f793d4 IntEx.thy
--- a/IntEx.thy	Fri Nov 27 07:16:16 2009 +0100
+++ b/IntEx.thy	Fri Nov 27 08:15:23 2009 +0100
@@ -142,7 +142,7 @@
 
 ML {*
 fun lift_tac_fset lthy t =
-  lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs
+  lift_tac lthy t [rel_eqv] rty [quot] trans2 rsp_thms defs
 *}
 
 lemma "PLUS a b = PLUS b a"
@@ -167,9 +167,12 @@
 lemma map_prs: "map REP_my_int (map ABS_my_int x) = x"
 sorry
 
+lemma foldl_prs: "((op \<approx> ===> op \<approx> ===> op \<approx>) ===> op \<approx> ===> op = ===> op \<approx>) foldl foldl"
+sorry
+
 lemma "foldl PLUS x [] = x"
 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
-apply (simp_all only: map_prs)
+apply (simp_all only: map_prs foldl_prs)
 sorry
 
 (*
@@ -187,8 +190,8 @@
 
 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 {* 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 *})
 oops