# HG changeset patch # User wenzelm # Date 1288725416 -3600 # Node ID 132e2349694bfc21dc897b1c27d57a4b2e26a7e5 # Parent 2bdb14323fbfda0b152ed118773a044c11a37175 avoid catch-all exception handling; diff -r 2bdb14323fbf -r 132e2349694b src/HOL/Matrix/Cplex_tools.ML --- a/src/HOL/Matrix/Cplex_tools.ML Tue Nov 02 20:15:57 2010 +0100 +++ b/src/HOL/Matrix/Cplex_tools.ML Tue Nov 02 20:16:56 2010 +0100 @@ -977,7 +977,6 @@ end handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) | Option => raise (Load_cplexResult "Option") - | x => raise x fun load_cplexResult name = let @@ -1127,7 +1126,6 @@ end handle (Tokenize s) => raise (Load_cplexResult ("Tokenize: "^s)) | Option => raise (Load_cplexResult "Option") - | x => raise x exception Execute of string; @@ -1153,7 +1151,7 @@ result end handle (Load_cplexResult s) => raise (Execute ("Load_cplexResult: "^s^"\nExecute: "^answer)) - | _ => raise (Execute answer) + | _ => raise (Execute answer) (* FIXME avoid handle _ *) end fun solve_cplex prog =