--- a/NEWS Thu Jul 09 17:34:59 2009 +0200
+++ b/NEWS Thu Jul 09 22:01:41 2009 +0200
@@ -92,6 +92,10 @@
*** ML ***
+* Renamed functor TableFun to Table, and GraphFun to Graph. (Since
+functors have their own ML name space there is no point to mark them
+separately.) Minor INCOMPATIBILITY.
+
* Renamed NamedThmsFun to Named_Thms. INCOMPATIBILITY.
* Eliminated old Attrib.add_attributes, Method.add_methods and related
--- a/src/HOL/Import/hol4rews.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Import/hol4rews.ML Thu Jul 09 22:01:41 2009 +0200
@@ -1,9 +1,8 @@
(* Title: HOL/Import/hol4rews.ML
- ID: $Id$
Author: Sebastian Skalberg (TU Muenchen)
*)
-structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord);
+structure StringPair = Table(type key = string * string val ord = prod_ord string_ord string_ord);
type holthm = (term * term) list * thm
--- a/src/HOL/Library/positivstellensatz.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Library/positivstellensatz.ML Thu Jul 09 22:01:41 2009 +0200
@@ -33,7 +33,7 @@
struct
type key = Key.key;
-structure Tab = TableFun(Key);
+structure Tab = Table(Key);
type 'a T = 'a Tab.table;
val undefined = Tab.empty;
--- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML Thu Jul 09 22:01:41 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
- ID: $Id$
Author: Steven Obua
*)
@@ -49,7 +48,7 @@
struct
type float = Float.float
-structure Inttab = TableFun(type key = int val ord = rev_order o int_ord);
+structure Inttab = Table(type key = int val ord = rev_order o int_ord);
type vector = string Inttab.table
type matrix = vector Inttab.table
--- a/src/HOL/Matrix/cplex/fspmlp.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Matrix/cplex/fspmlp.ML Thu Jul 09 22:01:41 2009 +0200
@@ -1,5 +1,4 @@
(* Title: HOL/Matrix/cplex/fspmlp.ML
- ID: $Id$
Author: Steven Obua
*)
@@ -45,9 +44,9 @@
(if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)
else GREATER
-structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
+structure Inttab = Table(type key = int val ord = (rev_order o int_ord));
-structure VarGraph = TableFun(type key = int*bound_type val ord = intbound_ord);
+structure VarGraph = Table(type key = int*bound_type val ord = intbound_ord);
(* key -> (float option) * (int -> (float * (((float * float) * key) list)))) *)
(* dest_key -> (sure_bound * (row_index -> (row_bound * (((coeff_lower * coeff_upper) * src_key) list)))) *)
--- a/src/HOL/Tools/Function/decompose.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Tools/Function/decompose.ML Thu Jul 09 22:01:41 2009 +0200
@@ -19,7 +19,7 @@
structure Decompose : DECOMPOSE =
struct
-structure TermGraph = GraphFun(type key = term val ord = TermOrd.fast_term_ord);
+structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord);
fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
--- a/src/HOL/Tools/Function/termination.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Tools/Function/termination.ML Thu Jul 09 22:01:41 2009 +0200
@@ -51,8 +51,8 @@
open FundefLib
val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
-structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
-structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
+structure Term2tab = Table(type key = term * term val ord = term2_ord);
+structure Term3tab = Table(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
(** Analyzing binary trees **)
--- a/src/HOL/Tools/res_atp.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/HOL/Tools/res_atp.ML Thu Jul 09 22:01:41 2009 +0200
@@ -152,7 +152,7 @@
end;
-structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
+structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
fun count_axiom_consts theory_const thy ((thm,_), tab) =
let fun count_const (a, T, tab) =
--- a/src/Pure/Concurrent/task_queue.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Pure/Concurrent/task_queue.ML Thu Jul 09 22:01:41 2009 +0200
@@ -41,7 +41,7 @@
fun str_of_task (Task (_, i)) = string_of_int i;
fun task_ord (Task t1, Task t2) = prod_ord (rev_order o int_ord) int_ord (t1, t2);
-structure Task_Graph = GraphFun(type key = task val ord = task_ord);
+structure Task_Graph = Graph(type key = task val ord = task_ord);
(* groups *)
--- a/src/Pure/General/graph.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Pure/General/graph.ML Thu Jul 09 22:01:41 2009 +0200
@@ -52,7 +52,7 @@
val extend: (key -> 'a * key list) -> key -> 'a T -> 'a T
end;
-functor GraphFun(Key: KEY): GRAPH =
+functor Graph(Key: KEY): GRAPH =
struct
(* keys *)
@@ -67,7 +67,7 @@
(* tables and sets of keys *)
-structure Table = TableFun(Key);
+structure Table = Table(Key);
type keys = unit Table.table;
val empty_keys = Table.empty: keys;
@@ -299,5 +299,5 @@
end;
-structure Graph = GraphFun(type key = string val ord = fast_string_ord);
-structure IntGraph = GraphFun(type key = int val ord = int_ord);
+structure Graph = Graph(type key = string val ord = fast_string_ord);
+structure IntGraph = Graph(type key = int val ord = int_ord);
--- a/src/Pure/General/table.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Pure/General/table.ML Thu Jul 09 22:01:41 2009 +0200
@@ -58,7 +58,7 @@
'a list table * 'a list table -> 'a list table (*exception DUP*)
end;
-functor TableFun(Key: KEY): TABLE =
+functor Table(Key: KEY): TABLE =
struct
@@ -409,8 +409,8 @@
end;
-structure Inttab = TableFun(type key = int val ord = int_ord);
-structure Symtab = TableFun(type key = string val ord = fast_string_ord);
-structure Symreltab = TableFun(type key = string * string
+structure Inttab = Table(type key = int val ord = int_ord);
+structure Symtab = Table(type key = string val ord = fast_string_ord);
+structure Symreltab = Table(type key = string * string
val ord = prod_ord fast_string_ord fast_string_ord);
--- a/src/Pure/Isar/code.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Pure/Isar/code.ML Thu Jul 09 22:01:41 2009 +0200
@@ -355,7 +355,7 @@
(* data slots dependent on executable code *)
(*private copy avoids potential conflict of table exceptions*)
-structure Datatab = TableFun(type key = int val ord = int_ord);
+structure Datatab = Table(type key = int val ord = int_ord);
local
--- a/src/Pure/context.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Pure/context.ML Thu Jul 09 22:01:41 2009 +0200
@@ -97,7 +97,7 @@
(* data kinds and access methods *)
(*private copy avoids potential conflict of table exceptions*)
-structure Datatab = TableFun(type key = int val ord = int_ord);
+structure Datatab = Table(type key = int val ord = int_ord);
local
--- a/src/Pure/more_thm.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Pure/more_thm.ML Thu Jul 09 22:01:41 2009 +0200
@@ -414,4 +414,4 @@
val op aconvc = Thm.aconvc;
-structure Thmtab = TableFun(type key = thm val ord = Thm.thm_ord);
+structure Thmtab = Table(type key = thm val ord = Thm.thm_ord);
--- a/src/Pure/term_ord.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Pure/term_ord.ML Thu Jul 09 22:01:41 2009 +0200
@@ -204,6 +204,6 @@
end;
-structure Vartab = TableFun(type key = indexname val ord = TermOrd.fast_indexname_ord);
-structure Typtab = TableFun(type key = typ val ord = TermOrd.typ_ord);
-structure Termtab = TableFun(type key = term val ord = TermOrd.fast_term_ord);
+structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_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/Code/code_preproc.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Tools/Code/code_preproc.ML Thu Jul 09 22:01:41 2009 +0200
@@ -253,7 +253,7 @@
type var = const * int;
structure Vargraph =
- GraphFun(type key = var val ord = prod_ord const_ord int_ord);
+ Graph(type key = var val ord = prod_ord const_ord int_ord);
datatype styp = Tyco of string * styp list | Var of var | Free;
--- a/src/Tools/Compute_Oracle/am_interpreter.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Tools/Compute_Oracle/am_interpreter.ML Thu Jul 09 22:01:41 2009 +0200
@@ -16,7 +16,7 @@
| CApp of closure * closure | CAbs of closure
| Closure of (closure list) * closure
-structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
+structure prog_struct = Table(type key = int*int val ord = prod_ord int_ord int_ord);
datatype program = Program of ((pattern * closure * (closure*closure) list) list) prog_struct.table
--- a/src/Tools/Compute_Oracle/compute.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Tools/Compute_Oracle/compute.ML Thu Jul 09 22:01:41 2009 +0200
@@ -167,7 +167,7 @@
| machine_of_prog (ProgHaskell _) = HASKELL
| machine_of_prog (ProgSML _) = SML
-structure Sorttab = TableFun(type key = sort val ord = TermOrd.sort_ord)
+structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord)
type naming = int -> string
--- a/src/Tools/Compute_Oracle/linker.ML Thu Jul 09 17:34:59 2009 +0200
+++ b/src/Tools/Compute_Oracle/linker.ML Thu Jul 09 22:01:41 2009 +0200
@@ -54,8 +54,8 @@
fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
-structure Consttab = TableFun(type key = constant val ord = constant_ord);
-structure ConsttabModTy = TableFun(type key = constant val ord = constant_modty_ord);
+structure Consttab = Table(type key = constant val ord = constant_ord);
+structure ConsttabModTy = Table(type key = constant val ord = constant_modty_ord);
fun typ_of_constant (Constant (_, _, ty)) = ty
@@ -72,7 +72,7 @@
fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
(list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B)
-structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord);
+structure Substtab = Table(type key = Type.tyenv val ord = subst_ord);
fun substtab_union c = Substtab.fold Substtab.update c
fun substtab_unions [] = Substtab.empty
@@ -382,7 +382,7 @@
fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
-structure CThmtab = TableFun (type key = cthm val ord = cthm_ord)
+structure CThmtab = Table(type key = cthm val ord = cthm_ord)
fun remove_duplicates ths =
let