# HG changeset patch
# User wenzelm
# Date 1453645832 -3600
# Node ID dd22d242304792f10dc2733ece6a811df39f68fa
# Parent  a4e6ea45f41622371007071b976c6165d5cf1023
clarified exception handling;

diff -r a4e6ea45f416 -r dd22d2423047 src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML
--- a/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sun Jan 24 15:25:39 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML	Sun Jan 24 15:30:32 2016 +0100
@@ -1070,9 +1070,7 @@
                  rec_inf_tac)
              end)
         fun ignore_interpretation_exn f x = SOME (f x)
-          handle
-              INTERPRET_INFERENCE => NONE
-            | exn => reraise exn
+          handle INTERPRET_INFERENCE => NONE
       in
         if List.null skel then
           raise SKELETON
diff -r a4e6ea45f416 -r dd22d2423047 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jan 24 15:25:39 2016 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jan 24 15:30:32 2016 +0100
@@ -875,8 +875,8 @@
         in
           use_candidate target_ty params' (candidate_param :: acc) val_ty
         end
-        handle TYPE ("dest_funT", _, _) => NONE
-             | DEST_LIST => NONE
+        handle TYPE ("dest_funT", _, _) => NONE  (* FIXME fragile *)
+             | _ => NONE  (* FIXME avoid catch-all handler *)
 
     val (skolem_const_ty, params') = skolem_const_info_of conclusion