eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;

--- a/src/HOL/Library/positivstellensatz.ML	Tue May 25 20:22:55 2010 +0200
+++ b/src/HOL/Library/positivstellensatz.ML	Tue May 25 20:28:16 2010 +0200
@@ -386,7 +386,7 @@
  fun real_ineq_conv th ct =
   let
    val th' = (Thm.instantiate (Thm.match (Thm.lhs_of th, ct)) th 
-      handle MATCH => raise CTERM ("real_ineq_conv", [ct]))
+      handle Pattern.MATCH => raise CTERM ("real_ineq_conv", [ct]))
   in Thm.transitive th' (oprconv poly_conv (Thm.rhs_of th'))
   end 
   val [real_lt_conv, real_le_conv, real_eq_conv,

--- a/src/HOL/Library/reflection.ML	Tue May 25 20:22:55 2010 +0200
+++ b/src/HOL/Library/reflection.ML	Tue May 25 20:28:16 2010 +0200
@@ -140,24 +140,25 @@
                    bds)
                end)
            | _ => da (s,ctxt) bds)
-      in (case cgns of
+      in
+        (case cgns of
           [] => tryabsdecomp (t,ctxt) bds
-        | ((vns,cong)::congs) => ((let
-            val cert = cterm_of thy
-            val certy = ctyp_of thy
-            val (tyenv, tmenv) =
-              Pattern.match thy
-                ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
-                (Vartab.empty, Vartab.empty)
-            val (fnvs,invs) = List.partition (fn ((vn,_),_) => member (op =) vns vn) (Vartab.dest tmenv)
-            val (fts,its) =
-              (map (snd o snd) fnvs,
-               map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
-            val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
-          in ((fts ~~ (replicate (length fts) ctxt),
-               Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
-          end)
-        handle MATCH => decomp_genreif da congs (t,ctxt) bds))
+        | ((vns,cong)::congs) =>
+            (let
+              val cert = cterm_of thy
+              val certy = ctyp_of thy
+              val (tyenv, tmenv) =
+                Pattern.match thy
+                  ((fst o HOLogic.dest_eq o HOLogic.dest_Trueprop) (concl_of cong), t)
+                  (Vartab.empty, Vartab.empty)
+              val (fnvs,invs) = List.partition (fn ((vn,_),_) => member (op =) vns vn) (Vartab.dest tmenv)
+              val (fts,its) =
+                (map (snd o snd) fnvs,
+                 map (fn ((vn,vi),(tT,t)) => (cert(Var ((vn,vi),tT)), cert t)) invs)
+              val ctyenv = map (fn ((vn,vi),(s,ty)) => (certy (TVar((vn,vi),s)), certy ty)) (Vartab.dest tyenv)
+            in ((fts ~~ (replicate (length fts) ctxt),
+                 Library.apfst (FWD (instantiate (ctyenv, its) cong))), bds)
+            end handle Pattern.MATCH => decomp_genreif da congs (t,ctxt) bds))
       end;
 
  (* looks for the atoms equation and instantiates it with the right number *)
@@ -231,7 +232,7 @@
               in map (fn (v,t) => (ih v, ih t)) (subst_ns@subst_vs@cts)  end
             val th = (instantiate (subst_ty, substt)  eq) RS sym
           in (hd (Variable.export ctxt'' ctxt [th]), bds) end)
-          handle MATCH => tryeqs eqs bds)
+          handle Pattern.MATCH => tryeqs eqs bds)
       in tryeqs (filter isat eqs) bds end), bds);
 
   (* Generic reification procedure: *)

--- a/src/HOL/Tools/Qelim/cooper.ML	Tue May 25 20:22:55 2010 +0200
+++ b/src/HOL/Tools/Qelim/cooper.ML	Tue May 25 20:28:16 2010 +0200
@@ -10,6 +10,7 @@
   val get: Proof.context -> entry
   val del: term list -> attribute
   val add: term list -> attribute 
+  exception COOPER of string
   val conv: Proof.context -> conv
   val tac: bool -> thm list -> thm list -> Proof.context -> int -> tactic
   val method: (Proof.context -> Method.method) context_parser

--- a/src/HOL/Tools/refute.ML	Tue May 25 20:22:55 2010 +0200
+++ b/src/HOL/Tools/refute.ML	Tue May 25 20:28:16 2010 +0200
@@ -588,7 +588,7 @@
         | NONE =>
           get_typedef_ax axioms
       end handle ERROR _         => get_typedef_ax axioms
-               | MATCH           => get_typedef_ax axioms
+               | TERM _          => get_typedef_ax axioms
                | Type.TYPE_MATCH => get_typedef_ax axioms)
   in
     get_typedef_ax (Theory.all_axioms_of thy)

--- a/src/HOL/Word/WordArith.thy	Tue May 25 20:22:55 2010 +0200
+++ b/src/HOL/Word/WordArith.thy	Tue May 25 20:28:16 2010 +0200
@@ -512,7 +512,9 @@
 
 fun uint_arith_tacs ctxt = 
   let
-    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
+    fun arith_tac' n t =
+      Arith_Data.verbose_arith_tac ctxt n t
+        handle Cooper.COOPER _ => Seq.empty;
     val cs = claset_of ctxt;
     val ss = simpset_of ctxt;
   in 
@@ -1074,7 +1076,9 @@
 
 fun unat_arith_tacs ctxt =   
   let
-    fun arith_tac' n t = Arith_Data.verbose_arith_tac ctxt n t handle COOPER => Seq.empty;
+    fun arith_tac' n t =
+      Arith_Data.verbose_arith_tac ctxt n t
+        handle Cooper.COOPER _ => Seq.empty;
     val cs = claset_of ctxt;
     val ss = simpset_of ctxt;
   in