src/HOL/Import/proof_kernel.ML

     in
         if not (idx = "") andalso u = "_"
         then SOME (newstr,valOf(Int.fromString idx))
         else NONE
     end
-    handle _ => NONE
+    handle _ => NONE  (* FIXME avoid handle _ *)
 
 fun rewrite_hol4_term t thy =
     let
         val hol4rews1 = map (Thm.transfer thy) (HOL4Rewrites.get thy)
         val hol4ss = Simplifier.theory_context thy empty_ss

             let
                 val th1 = (SOME (PureThy.get_thm thy thmname)
                            handle ERROR _ =>
                                   (case split_name thmname of
                                        SOME (listname,idx) => (SOME (List.nth(PureThy.get_thms thy listname,idx-1))
-                                                               handle _ => NONE)
+                                                               handle _ => NONE)  (* FIXME avoid handle _ *)
                                      | NONE => NONE))
             in
                 case th1 of
                     SOME th2 =>
                     (case Shuffler.set_prop thy isaconc [(thmname,th2)] of

                  prin lhs)
               | _ => ()
         end
   in
       case b of
-          NONE => (warn () handle _ => (); (a,b))
+          NONE => (warn () handle _ => (); (a,b)) (* FIXME avoid handle _ *)
         | _ => (a, b)
   end
 
 fun get_thm thyname thmname thy =
     case get_hol4_thm thyname thmname thy of