--- a/Quot/QuotMain.thy	Mon Dec 07 21:53:50 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 21:54:14 2009 +0100
@@ -1000,7 +1000,7 @@
 fun lambda_prs_simple_conv ctxt ctrm =
   case (term_of ctrm) of
    ((Const (@{const_name fun_map}, _) $ r1 $ a2) $ (Abs _)) =>
-     let
+     (let
        val thy = ProofContext.theory_of ctxt
        val (ty_b, ty_a) = dest_fun_type (fastype_of r1)
        val (ty_c, ty_d) = dest_fun_type (fastype_of a2)
@@ -1015,7 +1015,7 @@
            val (insp, inst) = make_inst (term_of (Thm.lhs_of ts)) (term_of ctrm)
          in
            Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) ts
-         end handle Bind =>
+         end handle _ => (* TODO handle only Bind | Error "make_inst" *)
          let
            val (insp, inst) = make_inst2 (term_of (Thm.lhs_of te)) (term_of ctrm)
            val td = Drule.instantiate ([], [(cterm_of thy insp, cterm_of thy inst)]) te
@@ -1032,6 +1032,7 @@
      in
        Conv.rewr_conv ti ctrm
      end
+     handle _ => Conv.all_conv ctrm)
   | _ => Conv.all_conv ctrm
 *}