diff -r 520a4084d064 -r b029f242d85d Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Tue Dec 08 17:30:00 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 17:33:51 2009 +0100
@@ -141,7 +141,7 @@
 done
 
 lemma "PLUS a b = PLUS a b"
-apply(lifting_setup rule: test1)
+apply(lifting_setup test1)
 apply(regularize)
 apply(injection)
 apply(cleaning)
@@ -203,7 +203,7 @@
 done
 
 lemma "foldl PLUS x [] = x"
-apply(lifting rule: ho_tst)
+apply(lifting ho_tst)
 apply(tactic {* clean_tac @{context} 1 *})
 apply(simp only: foldl_prs[OF Quotient_my_int Quotient_my_int] nil_prs[OF Quotient_my_int])
 done
@@ -343,7 +343,7 @@
 done
 
 lemma "map (\<lambda>x. PLUS x ZERO) l = l"
-apply(lifting rule: lam_tst4)
+apply(lifting lam_tst4)
 apply(cleaning)
 apply(simp only: babs_prs[OF Quotient_my_int Quotient_my_int])
 apply(simp only: map_prs[OF Quotient_my_int Quotient_my_int, symmetric])