src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
changeset 31971 8c1b845ed105
parent 24630 351a308ab58d
child 32740 9dd0a2f83429
     1.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Thu Jul 09 17:34:59 2009 +0200
     1.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Thu Jul 09 22:01:41 2009 +0200
     1.3 @@ -1,5 +1,4 @@
     1.4  (*  Title:      HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
     1.5 -    ID:         $Id$
     1.6      Author:     Steven Obua
     1.7  *)
     1.8  
     1.9 @@ -49,7 +48,7 @@
    1.10  struct
    1.11  
    1.12  type float = Float.float
    1.13 -structure Inttab = TableFun(type key = int val ord = rev_order o int_ord);
    1.14 +structure Inttab = Table(type key = int val ord = rev_order o int_ord);
    1.15  
    1.16  type vector = string Inttab.table
    1.17  type matrix = vector Inttab.table