--- a/Quot/Examples/IntEx.thy	Wed Jan 13 13:40:23 2010 +0100
+++ b/Quot/Examples/IntEx.thy	Wed Jan 13 13:40:47 2010 +0100
@@ -252,8 +252,7 @@
 apply(lifting lam_tst3a)
 apply(rule impI)
 apply(rule lam_tst3a_reg)
-(* INJECTION PROBLEM *)
-oops
+done
 
 lemma lam_tst3b: "(\<lambda>(y :: nat \<times> nat \<Rightarrow> nat \<times> nat). y) = (\<lambda>(x :: nat \<times> nat \<Rightarrow> nat \<times> nat). x)"
 by auto
@@ -263,10 +262,7 @@
 apply(rule impI)
 apply(rule babs_rsp[OF fun_quotient[OF Quotient_my_int Quotient_my_int]])
 apply(simp add: id_rsp)
-(* INJECTION PROBLEM --- possibly now id_def is part of id_simps again *)
-oops
-
-term map
+done
 
 lemma lam_tst4: "map (\<lambda>x. my_plus x (0,0)) l = l"
 apply (induct l)