# HG changeset patch
# User wenzelm
# Date 1121362100 -7200
# Node ID 131ca99f6abfb22e0e1466bb823f3c36b8bb9c20
# Parent  416e860889310d17384e115a94b06b72dbc4e371
use existing Inttab;

diff -r 416e86088931 -r 131ca99f6abf src/HOL/Matrix/cplex/CplexMatrixConverter.ML
--- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Thu Jul 14 19:28:19 2005 +0200
+++ b/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Thu Jul 14 19:28:20 2005 +0200
@@ -49,8 +49,6 @@
      
 exception Converter of string;
 
-structure Inttab = TableFun(type key = int val ord = int_ord);
-
 fun neg_term (cplexNeg t) = t
   | neg_term (cplexSum ts) = cplexSum (map neg_term ts)
   | neg_term t = cplexNeg t 
diff -r 416e86088931 -r 131ca99f6abf src/Pure/defs.ML
--- a/src/Pure/defs.ML	Thu Jul 14 19:28:19 2005 +0200
+++ b/src/Pure/defs.ML	Thu Jul 14 19:28:20 2005 +0200
@@ -197,8 +197,6 @@
       NONE => false
     | _ => true
            
-structure Inttab = TableFun(type key = int val ord = int_ord);
-
 fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
     if maxidx <= 1000000 then edge else
     let