use existing Inttab;
authorwenzelm
Thu Jul 14 19:28:20 2005 +0200 (2005-07-14)
changeset 16838131ca99f6abf
parent 16837 416e86088931
child 16839 d7b47195ac7b
use existing Inttab;
src/HOL/Matrix/cplex/CplexMatrixConverter.ML
src/Pure/defs.ML
     1.1 --- a/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Thu Jul 14 19:28:19 2005 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/CplexMatrixConverter.ML	Thu Jul 14 19:28:20 2005 +0200
     1.3 @@ -49,8 +49,6 @@
     1.4       
     1.5  exception Converter of string;
     1.6  
     1.7 -structure Inttab = TableFun(type key = int val ord = int_ord);
     1.8 -
     1.9  fun neg_term (cplexNeg t) = t
    1.10    | neg_term (cplexSum ts) = cplexSum (map neg_term ts)
    1.11    | neg_term t = cplexNeg t 
     2.1 --- a/src/Pure/defs.ML	Thu Jul 14 19:28:19 2005 +0200
     2.2 +++ b/src/Pure/defs.ML	Thu Jul 14 19:28:20 2005 +0200
     2.3 @@ -197,8 +197,6 @@
     2.4        NONE => false
     2.5      | _ => true
     2.6             
     2.7 -structure Inttab = TableFun(type key = int val ord = int_ord);
     2.8 -
     2.9  fun normalize_edge_idx (edge as (maxidx, u1, v1, history)) =
    2.10      if maxidx <= 1000000 then edge else
    2.11      let