src/Pure/context.ML
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