# HG changeset patch
# User wenzelm
# Date 1162924786 -3600
# Node ID 76d6d445d69b7346ff00bbb08e9f2e3f3d9cf549
# Parent  a607ae87ee81cb9a83016eece5f42f0a7b13729e
avoid handling of arbitrary exceptions;

diff -r a607ae87ee81 -r 76d6d445d69b src/Provers/hypsubst.ML
--- a/src/Provers/hypsubst.ML	Tue Nov 07 18:25:48 2006 +0100
+++ b/src/Provers/hypsubst.ML	Tue Nov 07 19:39:46 2006 +0100
@@ -109,8 +109,8 @@
         | eq_var_aux k (Const("==>",_) $ A $ B) =
               ((k, inspect_pair bnd novars
                     (Data.dest_eq (Data.dest_Trueprop A)))
-                      (*Exception comes from inspect_pair or dest_eq*)
-               handle _ => eq_var_aux (k+1) B)
+               handle TERM _ => eq_var_aux (k+1) B
+                 | Match => eq_var_aux (k+1) B)
         | eq_var_aux k _ = raise EQ_VAR
   in  eq_var_aux 0  end;
 
@@ -121,7 +121,7 @@
                                    (Data.dest_Trueprop (#prop (rep_thm th))))
       then th RS Data.eq_reflection
       else symmetric(th RS Data.eq_reflection) (*reorient*) ]
-    handle _ => [];  (*Exception comes from inspect_pair or dest_eq*)
+    handle TERM _ => [] | Match => [];
 
 local
 in