handle THM exn;

--- a/src/FOL/IFOL.ML	Sat Jul 10 21:43:27 1999 +0200
+++ b/src/FOL/IFOL.ML	Sat Jul 10 21:44:26 1999 +0200
@@ -248,7 +248,7 @@
 (*Apply an equality or definition ONCE.
   Fails unless the substitution has an effect*)
 fun stac th = 
-  let val th' = th RS meta_eq_to_obj_eq handle _ => th
+  let val th' = th RS meta_eq_to_obj_eq handle THM _ => th
   in  CHANGED_GOAL (rtac (th' RS ssubst))
   end;
 

--- a/src/Provers/simp.ML	Sat Jul 10 21:43:27 1999 +0200
+++ b/src/Provers/simp.ML	Sat Jul 10 21:44:26 1999 +0200
@@ -118,14 +118,14 @@
 
 fun find_res thms thm =
     let fun find [] = (prths thms; error"Check Simp_Data")
-          | find(th::thms) = thm RS th handle _ => find thms
+          | find(th::thms) = thm RS th handle THM _ => find thms
     in find thms end;
 
 val mk_trans = find_res trans_thms;
 
 fun mk_trans2 thm =
 let fun mk[] = error"Check transitivity"
-      | mk(t::ts) = (thm RSN (2,t))  handle _  => mk ts
+      | mk(t::ts) = (thm RSN (2,t))  handle THM _  => mk ts
 in mk trans_thms end;
 
 (*Applies tactic and returns the first resulting state, FAILS if none!*)