src/HOL/Matrix/Cplex_tools.ML
changeset 40299 132e2349694b
parent 37788 261c61fabc98
child 41490 0f1e411a1448
--- 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 =