diff -r b91782991dc8 -r 95ee248b3832 Quot/Examples/IntEx.thy
--- a/Quot/Examples/IntEx.thy	Thu Jan 21 11:11:22 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Thu Jan 21 12:03:47 2010 +0100
@@ -191,10 +191,6 @@
 
 lemma ex1tst': "\<exists>! (x :: my_int). x = x"
 apply(lifting ex1tst)
-
-apply injection
-apply (rule quot_respect(9))
-apply (rule Quotient_my_int)
 done
 
 lemma ho_tst: "foldl my_plus x [] = x"