handle THM/TERM exn;

--- a/src/HOL/Arith.ML	Sat Jul 10 21:46:15 1999 +0200
+++ b/src/HOL/Arith.ML	Sat Jul 10 21:48:27 1999 +0200
@@ -865,7 +865,7 @@
 val not_leD = linorder_not_le RS iffD1;
 
 
-fun mk_Eq thm = (thm RS Eq_FalseI) handle _ => (thm RS Eq_TrueI);
+fun mk_Eq thm = (thm RS Eq_FalseI) handle THM _ => (thm RS Eq_TrueI);
 
 val mk_Trueprop = HOLogic.mk_Trueprop;
 

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

--- a/src/HOL/simpdata.ML	Sat Jul 10 21:46:15 1999 +0200
+++ b/src/HOL/simpdata.ML	Sat Jul 10 21:48:27 1999 +0200
@@ -31,7 +31,7 @@
                     else  cla addSIs [th]
               | _ => cla addSIs [th],
        simp addsimps [th])
-      handle _ => error ("AddIffs: theorem must be unconditional\n" ^ 
+      handle TERM _ => error ("AddIffs: theorem must be unconditional\n" ^ 
                          string_of_thm th);
 
   fun delIff ((cla, simp), th) = 
@@ -45,7 +45,7 @@
                     else cla delrules [th]
               | _ => cla delrules [th],
        simp delsimps [th])
-      handle _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
+      handle TERM _ => (warning("DelIffs: ignoring conditional theorem\n" ^ 
                           string_of_thm th); (cla, simp));
 
   fun store_clasimp (cla, simp) = (claset_ref () := cla; simpset_ref () := simp)