src/Provers/Arith/fast_lin_arith.ML

                                         then LA_Data.decomp sg (concl_of thm)
                                         else None) asms)
 
       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
         | try_add (thm1::thm1s) thm2 = case add2 thm1 thm2 of
              None => try_add thm1s thm2 | some => some;

         let fun mul(i,th) = if i=1 then th else mul(i-1, addthms thm th)
         in if n < 0 then mul(~n,thm) RS LA_Logic.sym else mul(n,thm) end;
 
       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
 
       fun simp thm =
         let val thm' = trace_thm "Simplified:" (full_simplify simpset thm)

     let val (thm1,js1) = fwdproof sg tree1 js
         val (thm2,js2) = fwdproof sg tree2 js1
         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
     val cnTconcl = cterm_of sg nTconcl
     val nTconclthm = assume cnTconcl