diff -r 1dd6a21cdd1c -r 58947b7232ef IntEx.thy
--- a/IntEx.thy	Thu Nov 26 02:31:00 2009 +0100
+++ b/IntEx.thy	Thu Nov 26 03:18:38 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
 
 (*