src/Tools/Compute_Oracle/linker.ML
changeset 31971 8c1b845ed105
parent 29275 9fa69e3858d6
child 32035 8e77b6a250d5
     1.1 --- a/src/Tools/Compute_Oracle/linker.ML	Thu Jul 09 17:34:59 2009 +0200
     1.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Thu Jul 09 22:01:41 2009 +0200
     1.3 @@ -54,8 +54,8 @@
     1.4  fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
     1.5  
     1.6  
     1.7 -structure Consttab = TableFun(type key = constant val ord = constant_ord);
     1.8 -structure ConsttabModTy = TableFun(type key = constant val ord = constant_modty_ord);
     1.9 +structure Consttab = Table(type key = constant val ord = constant_ord);
    1.10 +structure ConsttabModTy = Table(type key = constant val ord = constant_modty_ord);
    1.11  
    1.12  fun typ_of_constant (Constant (_, _, ty)) = ty
    1.13  
    1.14 @@ -72,7 +72,7 @@
    1.15  fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
    1.16      (list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B)
    1.17  
    1.18 -structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord);
    1.19 +structure Substtab = Table(type key = Type.tyenv val ord = subst_ord);
    1.20  
    1.21  fun substtab_union c = Substtab.fold Substtab.update c
    1.22  fun substtab_unions [] = Substtab.empty
    1.23 @@ -382,7 +382,7 @@
    1.24  
    1.25  fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
    1.26  
    1.27 -structure CThmtab = TableFun (type key = cthm val ord = cthm_ord)
    1.28 +structure CThmtab = Table(type key = cthm val ord = cthm_ord)
    1.29  
    1.30  fun remove_duplicates ths =
    1.31      let