--- a/Quot/QuotMain.thy	Mon Dec 14 10:09:49 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 14 10:12:23 2009 +0100
@@ -719,6 +719,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)
 *}