changeset 31971 | 8c1b845ed105 |
parent 30628 | 4078276bcace |
child 32738 | 15bb09ca0378 |
--- a/src/Pure/context.ML Thu Jul 09 17:34:59 2009 +0200 +++ b/src/Pure/context.ML Thu Jul 09 22:01:41 2009 +0200 @@ -97,7 +97,7 @@ (* data kinds and access methods *) (*private copy avoids potential conflict of table exceptions*) -structure Datatab = TableFun(type key = int val ord = int_ord); +structure Datatab = Table(type key = int val ord = int_ord); local