Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clarified exception handling;
authorwenzelm
Sun, 24 Jan 2016 15:30:32 +0100
changeset 62243 dd22d2423047
parent 62242 a4e6ea45f416
child 62244 5d513565749e
clarified exception handling;
src/HOL/TPTP/TPTP_Parser/tptp_reconstruct.ML file | annotate | diff | comparison | revisions
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy file | annotate | diff | comparison | revisions 
--- 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
--- 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
isabelle