# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1260217317 -3600
# Node ID 678315da994ee61046e6b46fcd447e22c22bde86
# Parent  a8c3fa5c4015eb9e7485b946b9cede487eee901c
Handling of errors in lambda_prs_conv.

diff -r a8c3fa5c4015 -r 678315da994e Quot/QuotMain.thy
--- a/Quot/QuotMain.thy	Mon Dec 07 21:21:23 2009 +0100
+++ b/Quot/QuotMain.thy	Mon Dec 07 21:21:57 2009 +0100
@@ -1006,7 +1006,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)
@@ -1021,7 +1021,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
@@ -1038,6 +1038,7 @@
      in
        Conv.rewr_conv ti ctrm
      end
+     handle _ => Conv.all_conv ctrm)
   | _ => Conv.all_conv ctrm
 *}