--- a/Quot/QuotMain.thy	Wed Dec 09 16:44:34 2009 +0100
+++ b/Quot/QuotMain.thy	Wed Dec 09 17:05:33 2009 +0100
@@ -149,7 +149,6 @@
 lemmas [quot_respect] = quot_rel_rsp
 
 (* fun_map is not here since equivp is not true *)
-(* TODO: option, ... *)
 lemmas [quot_equiv] = identity_equivp
 
 (* definition of the quotient types *)
@@ -208,15 +207,10 @@
 
 section {* Infrastructure about id *}
 
-(* TODO: think where should this be *)
-lemma prod_fun_id: "prod_fun id id \<equiv> id"
-  by (rule eq_reflection) (simp add: prod_fun_def)
-
-lemmas [id_simps] = 
+lemmas [id_simps] =
   fun_map_id[THEN eq_reflection]
   id_apply[THEN eq_reflection]
   id_def[THEN eq_reflection,symmetric]
-  prod_fun_id
 
 section {* Debugging infrastructure for testing tactics *}
 
@@ -650,21 +644,6 @@
 handle _ => error "solve_quotient_assums failed. Maybe a quotient_thm is missing"
 *}
 
-(* Not used *)
-(* It proves the Quotient assumptions by calling quotient_tac *)
-ML {*
-fun solve_quotient_assum i ctxt thm =
-  let
-    val tac =
-      (compose_tac (false, thm, i)) THEN_ALL_NEW
-      (quotient_tac ctxt);
-    val gc = Drule.strip_imp_concl (cprop_of thm);
-  in
-    Goal.prove_internal [] gc (fn _ => tac 1)
-  end
-  handle _ => error "solve_quotient_assum"
-*}
-
 definition
   "QUOT_TRUE x \<equiv> True"