avoid catch-all exception handling;
authorwenzelm
Tue, 02 Nov 2010 20:16:56 +0100
changeset 40299 132e2349694b
parent 40298 2bdb14323fbf
child 40300 d4487353b3a0
child 40308 628dc6f24ddf
avoid catch-all exception handling;
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 =