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