# HG changeset patch
# User wenzelm
# Date 931636249 -7200
# Node ID 441393b452c76ba70061e64320adad2a4329fbe2
# Parent  7f2977e96a5c2e312a163142912fdfe52ec82e68
handle THM exn;

diff -r 7f2977e96a5c -r 441393b452c7 src/FOLP/simp.ML
--- a/src/FOLP/simp.ML	Sat Jul 10 21:48:27 1999 +0200
+++ b/src/FOLP/simp.ML	Sat Jul 10 21:50:49 1999 +0200
@@ -124,14 +124,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!*)