# HG changeset patch
# User wenzelm
# Date 1695922820 -7200
# Node ID 1b052426a2b753d19d6d2ee971f63108aed521ea
# Parent  810eca7539197ab79fd5ba10bfafb9030370509d
avoid accidental 'handle' of interrupts;

diff -r 810eca753919 -r 1b052426a2b7 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu Sep 28 19:36:54 2023 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu Sep 28 19:40:20 2023 +0200
@@ -75,6 +75,11 @@
   tptp_informative_failure = true
 ]]
 
+ML \<open>
+exception UNSUPPORTED_ROLE
+exception INTERPRET_INFERENCE
+\<close>
+
 ML_file \<open>TPTP_Parser/tptp_reconstruct_library.ML\<close>
 ML "open TPTP_Reconstruct_Library"
 ML_file \<open>TPTP_Parser/tptp_reconstruct.ML\<close>
@@ -867,16 +872,18 @@
           SOME (rev acc)
         else NONE
       else
-        let
-          val (arg_ty, val_ty) = Term.dest_funT cur_ty
-          (*now find a param of type arg_ty*)
-          val (candidate_param, params') =
-            find_and_remove (snd #> pair arg_ty #> (op =)) params
-        in
-          use_candidate target_ty params' (candidate_param :: acc) val_ty
-        end
-        handle TYPE ("dest_funT", _, _) => NONE  (* FIXME fragile *)
+        \<^try>\<open>
+          let
+            val (arg_ty, val_ty) = Term.dest_funT cur_ty
+            (*now find a param of type arg_ty*)
+            val (candidate_param, params') =
+              find_and_remove (snd #> pair arg_ty #> (op =)) params
+          in
+            use_candidate target_ty params' (candidate_param :: acc) val_ty
+          end
+          catch TYPE ("dest_funT", _, _) => NONE  (* FIXME fragile *)
              | _ => NONE  (* FIXME avoid catch-all handler *)
+        \<close>
 
     val (skolem_const_ty, params') = skolem_const_info_of conclusion
 
@@ -2012,9 +2019,6 @@
 subsection "Leo2 reconstruction tactic"
 
 ML \<open>
-exception UNSUPPORTED_ROLE
-exception INTERPRET_INFERENCE
-
 (*Failure reports can be adjusted to avoid interrupting
   an overall reconstruction process*)
 fun fail ctxt x =
diff -r 810eca753919 -r 1b052426a2b7 src/HOL/TPTP/TPTP_Test.thy
--- a/src/HOL/TPTP/TPTP_Test.thy	Thu Sep 28 19:36:54 2023 +0200
+++ b/src/HOL/TPTP/TPTP_Test.thy	Thu Sep 28 19:40:20 2023 +0200
@@ -56,15 +56,11 @@
     let
       val _ = TPTP_Syntax.debug tracing (msg ^ " " ^ Path.print file_name)
     in
-     (f file_name; ())
+     \<^try>\<open>(f file_name; ()) catch exn =>
      (*otherwise report exceptions as warnings*)
-     handle exn =>
-       if Exn.is_interrupt exn then
-         Exn.reraise exn
-       else
-         (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
-          " raised exception: " ^ Runtime.exn_message exn);
-          default_val)
+       (report ctxt (msg ^ " test: file " ^ Path.print file_name ^
+        " raised exception: " ^ Runtime.exn_message exn);
+        default_val)\<close>
     end
 
   fun timed_test ctxt f test_files =