tuned -- avoid catch-all exception pattern;

--- a/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue May 25 11:13:49 2010 +0200
+++ b/src/HOL/Matrix/cplex/Cplex_tools.ML	Tue May 25 20:22:55 2010 +0200
@@ -730,9 +730,7 @@
 
 fun mergemap f ts = fold (fn x => fn table => merge table (f x)) ts Symtab.empty
 
-fun diff a b = Symtab.fold (fn (k, v) => fn a =>
-             (Symtab.delete k a) handle UNDEF => a)
-             b a
+fun diff a b = Symtab.fold (Symtab.delete_safe o fst) b a
 
 fun collect_vars (cplexVar v) = singleton v
   | collect_vars (cplexNeg t) = collect_vars t