# HG changeset patch
# User wenzelm
# Date 1247169701 -7200
# Node ID 8c1b845ed1057d989b117b87b7dab15293fefb43
# Parent  ccaadfcf6941479b71b97e935ea95c9a4747a2e4
renamed functor TableFun to Table, and GraphFun to Graph;

diff -r ccaadfcf6941 -r 8c1b845ed105 NEWS
--- 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
diff -r ccaadfcf6941 -r 8c1b845ed105 src/HOL/Import/hol4rews.ML
--- 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
 
diff -r ccaadfcf6941 -r 8c1b845ed105 src/HOL/Library/positivstellensatz.ML
--- 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;
diff -r ccaadfcf6941 -r 8c1b845ed105 src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
--- 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
diff -r ccaadfcf6941 -r 8c1b845ed105 src/HOL/Matrix/cplex/fspmlp.ML
--- 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)))) *)
 
diff -r ccaadfcf6941 -r 8c1b845ed105 src/HOL/Tools/Function/decompose.ML
--- 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) =>
diff -r ccaadfcf6941 -r 8c1b845ed105 src/HOL/Tools/Function/termination.ML
--- 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 **)
 
diff -r ccaadfcf6941 -r 8c1b845ed105 src/HOL/Tools/res_atp.ML
--- 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) =
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Pure/Concurrent/task_queue.ML
--- 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 *)
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Pure/General/graph.ML
--- 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);
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Pure/General/table.ML
--- 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);
 
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Pure/Isar/code.ML
--- 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
 
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Pure/context.ML
--- 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
 
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Pure/more_thm.ML
--- 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);
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Pure/term_ord.ML
--- 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);
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Tools/Code/code_preproc.ML
--- 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;
 
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Tools/Compute_Oracle/am_interpreter.ML
--- 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
 
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Tools/Compute_Oracle/compute.ML
--- 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
 
diff -r ccaadfcf6941 -r 8c1b845ed105 src/Tools/Compute_Oracle/linker.ML
--- 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