--- 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 =