# HG changeset patch
# User wenzelm
# Date 1085835597 -7200
# Node ID 241d2db86fc203727f724d3e4e934353795faacc
# Parent  3f80d6510ee99a4c7119fcf20e3214f7d552e1e1
avoid 'handle _' -- would cover Interrupt as well!!!

diff -r 3f80d6510ee9 -r 241d2db86fc2 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sat May 29 14:59:24 2004 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sat May 29 14:59:57 2004 +0200
@@ -429,7 +429,7 @@
 
       fun add2 thm1 thm2 =
         let val conj = thm1 RS (thm2 RS LA_Logic.conjI)
-        in get_first (fn th => Some(conj RS th) handle _ => None) add_mono_thms
+        in get_first (fn th => Some(conj RS th) handle THM _ => None) add_mono_thms
         end;
 
       fun try_add [] _ = None
@@ -453,7 +453,7 @@
 
       fun multn2(n,thm) =
         let val Some(mth,cv) =
-              get_first (fn (th,cv) => Some(thm RS th,cv) handle _ => None) mult_mono_thms
+              get_first (fn (th,cv) => Some(thm RS th,cv) handle THM _ => None) mult_mono_thms
             val ct = cterm_of sg (LA_Data.number_of(n,#T(rep_cterm cv)))
         in instantiate ([],[(cv,ct)]) mth end
 
@@ -695,7 +695,7 @@
         val thm1' = implies_intr ct1 thm1
         val thm2' = implies_intr ct2 thm2
     in (thm2' COMP (thm1' COMP thm), js2) end;
-(* needs handle _ => None ? *)
+(* needs handle THM _ => None ? *)
 
 fun prover sg thms Tconcl js pos =
 let val nTconcl = LA_Logic.neg_prop Tconcl