| changeset 31971 | 8c1b845ed105 |
| parent 31962 | baa8dce5bc45 |
| child 31998 | 2c7a24f74db9 |
--- a/src/Pure/Isar/code.ML Thu Jul 09 17:34:59 2009 +0200 +++ b/src/Pure/Isar/code.ML Thu Jul 09 22:01:41 2009 +0200 @@ -355,7 +355,7 @@ (* data slots dependent on executable code *) (*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