--- a/Quot/QuotMain.thy	Thu Dec 10 10:36:05 2009 +0100
+++ b/Quot/QuotMain.thy	Thu Dec 10 10:54:45 2009 +0100
@@ -345,7 +345,9 @@
        else raise (LIFT_MATCH "regularize (bounds mismatch)")
 
   | (rt, qt) =>
-       raise (LIFT_MATCH "regularize failed (default)")
+       let val (rts, qts) = (Syntax.string_of_term lthy rt, Syntax.string_of_term lthy qt) in
+       raise (LIFT_MATCH ("regularize failed (default: " ^ rts ^ "," ^ qts ^ ")"))
+       end
 *}
 
 section {* Regularize Tactic *}