# HG changeset patch
# User wenzelm
# Date 931635866 -7200
# Node ID cfa87aef9ccdad81c1d50c3d9553c43f9613063e
# Parent  a766de7529960b7936ea8875f7c026546e8147a9
handle THM exn;

diff -r a766de752996 -r cfa87aef9ccd src/FOL/IFOL.ML
--- 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;
 
diff -r a766de752996 -r cfa87aef9ccd src/Provers/simp.ML
--- 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!*)