--- a/IntEx.thy	Wed Nov 25 15:43:12 2009 +0100
+++ b/IntEx.thy	Wed Nov 25 21:48:32 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 defs
+  lift_tac lthy t rel_eqv rel_refl rty quot trans2 rsp_thms reps_same absrep defs
 *}
 
 lemma "PLUS a b = PLUS b a"
@@ -166,8 +166,6 @@
 
 lemma "foldl PLUS x [] = x"
 apply (tactic {* lift_tac_fset @{context} @{thm ho_tst} 1 *})
-prefer 3
-apply(tactic {* clean_tac @{context} quot @{thms PLUS_def} reps_same 1 *})
 sorry
 
 (*