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