--- a/QuotMain.thy	Sun Dec 06 06:41:52 2009 +0100
+++ b/QuotMain.thy	Sun Dec 06 06:58:24 2009 +0100
@@ -797,7 +797,8 @@
   in
     case find_first find_fun asms of
       SOME (_ $ (_ $ (f $ a))) => (f, a)
-    | _ => error "find_qt_asm"
+    | SOME _ => error "find_qt_asm: no pair"
+    | NONE => error "find_qt_asm: no assumption"
   end
 *}
 
@@ -828,7 +829,7 @@
   Subgoal.FOCUS (fn {concl, asms, context,...} =>
     case ((HOLogic.dest_Trueprop (term_of concl))) of
       ((R2 $ (f $ x) $ (g $ y))) =>
-        let
+        (let
           val (asmf, asma) = find_qt_asm (map term_of asms);
         in
           if (fastype_of asmf) = (fastype_of f) then no_tac else let
@@ -845,6 +846,7 @@
             compose_tac (false, thm, 2) 1
           end
         end
+        handle ERROR "find_qt_asm: no pair" => no_tac)
     | _ => no_tac)
 *}