Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Sorttab in Pure;
authorwenzelm
Thu, 09 Jul 2009 22:36:11 +0200
changeset 31976 17414e2736f4
parent 31975 366ad09d39ef
child 31977 e03059ae2d82
Sorttab in Pure;
src/Pure/term_ord.ML file | annotate | diff | comparison | revisions
src/Tools/Compute_Oracle/compute.ML file | annotate | diff | comparison | revisions 
--- 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);
--- 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
isabelle