# HG changeset patch
# User wenzelm
# Date 1247171771 -7200
# Node ID 17414e2736f406d6426c7d45810229e7fe7e191f
# Parent  366ad09d39ef9825080a14f7636d70d5d4bd50d1
Sorttab in Pure;

diff -r 366ad09d39ef -r 17414e2736f4 src/Pure/term_ord.ML
--- a/src/Pure/term_ord.ML	Thu Jul 09 22:13:19 2009 +0200
+++ b/src/Pure/term_ord.ML	Thu Jul 09 22:36:11 2009 +0200
@@ -205,5 +205,6 @@
 end;
 
 structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord);
+structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord);
 structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord);
 structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord);
diff -r 366ad09d39ef -r 17414e2736f4 src/Tools/Compute_Oracle/compute.ML
--- a/src/Tools/Compute_Oracle/compute.ML	Thu Jul 09 22:13:19 2009 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML	Thu Jul 09 22:36:11 2009 +0200
@@ -167,8 +167,6 @@
   | machine_of_prog (ProgHaskell _) = HASKELL
   | machine_of_prog (ProgSML _) = SML
 
-structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord)
-
 type naming = int -> string
 
 fun default_naming i = "v_" ^ Int.toString i