# HG changeset patch
# User wenzelm
# Date 1274811775 -7200
# Node ID e32cc5958282cf554b18a4f72780efd894c6da04
# Parent  9b27c3dccb01f1b837aec8db4f79adac7a0a2f8f
tuned -- avoid catch-all exception pattern;

diff -r 9b27c3dccb01 -r e32cc5958282 src/HOL/Matrix/cplex/Cplex_tools.ML
--- 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