Sorttab in Pure;
authorwenzelm
Thu Jul 09 22:36:11 2009 +0200 (2009-07-09)
changeset 3197617414e2736f4
parent 31975 366ad09d39ef
child 31977 e03059ae2d82
Sorttab in Pure;
src/Pure/term_ord.ML
src/Tools/Compute_Oracle/compute.ML
     1.1 --- a/src/Pure/term_ord.ML	Thu Jul 09 22:13:19 2009 +0200
     1.2 +++ b/src/Pure/term_ord.ML	Thu Jul 09 22:36:11 2009 +0200
     1.3 @@ -205,5 +205,6 @@
     1.4  end;
     1.5  
     1.6  structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord);
     1.7 +structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord);
     1.8  structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord);
     1.9  structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord);
     2.1 --- a/src/Tools/Compute_Oracle/compute.ML	Thu Jul 09 22:13:19 2009 +0200
     2.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Thu Jul 09 22:36:11 2009 +0200
     2.3 @@ -167,8 +167,6 @@
     2.4    | machine_of_prog (ProgHaskell _) = HASKELL
     2.5    | machine_of_prog (ProgSML _) = SML
     2.6  
     2.7 -structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord)
     2.8 -
     2.9  type naming = int -> string
    2.10  
    2.11  fun default_naming i = "v_" ^ Int.toString i