# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260781943 -3600
# Node ID 7092bd4fd26431630247248c457508debca74609
# Parent  4b3822d1ed24459336f09cc8c7fbe8e19bdb291d
Reply in code.

diff -r 4b3822d1ed24 -r 7092bd4fd264 Quot/QuotMain.thy
--- 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)
 *}