--- a/Quot/Examples/IntEx.thy	Tue Dec 08 16:56:37 2009 +0100
+++ b/Quot/Examples/IntEx.thy	Tue Dec 08 16:56:51 2009 +0100
@@ -141,10 +141,10 @@
 done
 
 lemma "PLUS a b = PLUS a b"
-apply(tactic {* procedure_tac @{context} @{thm test1} 1 *})
-apply(tactic {* regularize_tac @{context} 1 *})
-apply(tactic {* all_inj_repabs_tac @{context} 1*})
-apply(tactic {* clean_tac @{context} 1 *}) 
+apply(lifting_setup rule: test1)
+apply(regularize)
+apply(injection)
+apply(cleaning)
 done
 
 thm lambda_prs