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!*)