--- a/Quot/Examples/FSet3.thy	Mon Dec 14 13:56:24 2009 +0100
+++ b/Quot/Examples/FSet3.thy	Mon Dec 14 13:57:39 2009 +0100
@@ -280,7 +280,7 @@
 sorry
 
 thm card_raw_cons_gt_0
-(*thm mem_card_raw_not_0*)
+thm mem_card_raw_gt_0
 thm not_nil_equiv_cons
 thm delete_raw.simps
 (*thm mem_delete_raw*)

--- a/Quot/QuotMain.thy	Mon Dec 14 13:56:24 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 14 13:57:39 2009 +0100
@@ -660,7 +660,8 @@
 
 ML {*
 (* FIXME / TODO: what is asmf and asma in the code below *)
-
+(* asmf is the QUOT_TRUE assumption function
+   asma are    QUOT_TRUE assumption arguments *)
 val apply_rsp_tac =
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
   let
@@ -719,6 +720,8 @@
            (rtac inst_thm THEN' quotient_tac ctxt) i
          end
          handle _ => no_tac) (* FIXME / TODO what is the catch for ? Should go away, no? *)
+(* The catch was for an error of solve_quotient_assum. You replaced it by quotient_tac
+   so I suppose it is equivalent to a "SOLVES" around quotient_tac. *)
     | _ => no_tac)
 *}