--- a/QuotMain.thy	Wed Nov 25 14:16:33 2009 +0100
+++ b/QuotMain.thy	Wed Nov 25 14:25:29 2009 +0100
@@ -1115,6 +1115,8 @@
   in
     Conv.rewr_conv ti ctrm
   end
+(* TODO: We can add a proper error message... *)
+  handle Bind => Conv.all_conv ctrm
 
 *}
 ML {*