# HG changeset patch
# User wenzelm
# Date 1118311409 -7200
# Node ID b146c31a29552a7b1dfff705a4acd505a91724f6
# Parent  e573e5167eda36d28c8ec7b03d4dcd54eddb0f89
added structure Inttab;
tuned comments;

diff -r e573e5167eda -r b146c31a2955 src/Pure/General/table.ML
--- a/src/Pure/General/table.ML	Thu Jun 09 12:03:28 2005 +0200
+++ b/src/Pure/General/table.ML	Thu Jun 09 12:03:29 2005 +0200
@@ -2,8 +2,8 @@
     ID:         $Id$
     Author:     Markus Wenzel and Stefan Berghofer, TU Muenchen
 
-Generic tables and tables indexed by strings.  Efficient purely
-functional implementation using balanced 2-3 trees.
+Generic tables.  Efficient purely functional implementation using
+balanced 2-3 trees.
 *)
 
 signature KEY =
@@ -341,6 +341,5 @@
 
 end;
 
-
-(*tables indexed by strings*)
+structure Inttab = TableFun(type key = int val ord = int_ord);
 structure Symtab = TableFun(type key = string val ord = string_ord);