renamed functor TableFun to Table, and GraphFun to Graph;
authorwenzelm
Thu Jul 09 22:01:41 2009 +0200 (2009-07-09)
changeset 319718c1b845ed105
parent 31970 ccaadfcf6941
child 31973 a89f758dba5b
renamed functor TableFun to Table, and GraphFun to Graph;
NEWS
src/HOL/Import/hol4rews.ML
src/HOL/Library/positivstellensatz.ML
src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
src/HOL/Matrix/cplex/fspmlp.ML
src/HOL/Tools/Function/decompose.ML
src/HOL/Tools/Function/termination.ML
src/HOL/Tools/res_atp.ML
src/Pure/Concurrent/task_queue.ML
src/Pure/General/graph.ML
src/Pure/General/table.ML
src/Pure/Isar/code.ML
src/Pure/context.ML
src/Pure/more_thm.ML
src/Pure/term_ord.ML
src/Tools/Code/code_preproc.ML
src/Tools/Compute_Oracle/am_interpreter.ML
src/Tools/Compute_Oracle/compute.ML
src/Tools/Compute_Oracle/linker.ML
     1.1 --- a/NEWS	Thu Jul 09 17:34:59 2009 +0200
     1.2 +++ b/NEWS	Thu Jul 09 22:01:41 2009 +0200
     1.3 @@ -92,6 +92,10 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Renamed functor TableFun to Table, and GraphFun to Graph.  (Since
     1.8 +functors have their own ML name space there is no point to mark them
     1.9 +separately.)  Minor INCOMPATIBILITY.
    1.10 +
    1.11  * Renamed NamedThmsFun to Named_Thms.  INCOMPATIBILITY.
    1.12  
    1.13  * Eliminated old Attrib.add_attributes, Method.add_methods and related
     2.1 --- a/src/HOL/Import/hol4rews.ML	Thu Jul 09 17:34:59 2009 +0200
     2.2 +++ b/src/HOL/Import/hol4rews.ML	Thu Jul 09 22:01:41 2009 +0200
     2.3 @@ -1,9 +1,8 @@
     2.4  (*  Title:      HOL/Import/hol4rews.ML
     2.5 -    ID:         $Id$
     2.6      Author:     Sebastian Skalberg (TU Muenchen)
     2.7  *)
     2.8  
     2.9 -structure StringPair = TableFun(type key = string * string val ord = prod_ord string_ord string_ord);
    2.10 +structure StringPair = Table(type key = string * string val ord = prod_ord string_ord string_ord);
    2.11  
    2.12  type holthm = (term * term) list * thm
    2.13  
     3.1 --- a/src/HOL/Library/positivstellensatz.ML	Thu Jul 09 17:34:59 2009 +0200
     3.2 +++ b/src/HOL/Library/positivstellensatz.ML	Thu Jul 09 22:01:41 2009 +0200
     3.3 @@ -33,7 +33,7 @@
     3.4  struct
     3.5  
     3.6  type key = Key.key;
     3.7 -structure Tab = TableFun(Key);
     3.8 +structure Tab = Table(Key);
     3.9  type 'a T = 'a Tab.table;
    3.10  
    3.11  val undefined = Tab.empty;
     4.1 --- a/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Thu Jul 09 17:34:59 2009 +0200
     4.2 +++ b/src/HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML	Thu Jul 09 22:01:41 2009 +0200
     4.3 @@ -1,5 +1,4 @@
     4.4  (*  Title:      HOL/Matrix/cplex/FloatSparseMatrixBuilder.ML
     4.5 -    ID:         $Id$
     4.6      Author:     Steven Obua
     4.7  *)
     4.8  
     4.9 @@ -49,7 +48,7 @@
    4.10  struct
    4.11  
    4.12  type float = Float.float
    4.13 -structure Inttab = TableFun(type key = int val ord = rev_order o int_ord);
    4.14 +structure Inttab = Table(type key = int val ord = rev_order o int_ord);
    4.15  
    4.16  type vector = string Inttab.table
    4.17  type matrix = vector Inttab.table
     5.1 --- a/src/HOL/Matrix/cplex/fspmlp.ML	Thu Jul 09 17:34:59 2009 +0200
     5.2 +++ b/src/HOL/Matrix/cplex/fspmlp.ML	Thu Jul 09 22:01:41 2009 +0200
     5.3 @@ -1,5 +1,4 @@
     5.4  (*  Title:      HOL/Matrix/cplex/fspmlp.ML
     5.5 -    ID:         $Id$
     5.6      Author:     Steven Obua
     5.7  *)
     5.8  
     5.9 @@ -45,9 +44,9 @@
    5.10          (if b1 = b2 then EQUAL else if b1=LOWER then LESS else GREATER)
    5.11      else GREATER
    5.12  
    5.13 -structure Inttab = TableFun(type key = int val ord = (rev_order o int_ord));
    5.14 +structure Inttab = Table(type key = int val ord = (rev_order o int_ord));
    5.15  
    5.16 -structure VarGraph = TableFun(type key = int*bound_type val ord = intbound_ord);
    5.17 +structure VarGraph = Table(type key = int*bound_type val ord = intbound_ord);
    5.18  (* key -> (float option) * (int -> (float * (((float * float) * key) list)))) *)
    5.19  (* dest_key -> (sure_bound * (row_index -> (row_bound * (((coeff_lower * coeff_upper) * src_key) list)))) *)
    5.20  
     6.1 --- a/src/HOL/Tools/Function/decompose.ML	Thu Jul 09 17:34:59 2009 +0200
     6.2 +++ b/src/HOL/Tools/Function/decompose.ML	Thu Jul 09 22:01:41 2009 +0200
     6.3 @@ -19,7 +19,7 @@
     6.4  structure Decompose : DECOMPOSE =
     6.5  struct
     6.6  
     6.7 -structure TermGraph = GraphFun(type key = term val ord = TermOrd.fast_term_ord);
     6.8 +structure TermGraph = Graph(type key = term val ord = TermOrd.fast_term_ord);
     6.9  
    6.10  
    6.11  fun derive_chains ctxt chain_tac cont D = Termination.CALLS (fn (cs, i) =>
     7.1 --- a/src/HOL/Tools/Function/termination.ML	Thu Jul 09 17:34:59 2009 +0200
     7.2 +++ b/src/HOL/Tools/Function/termination.ML	Thu Jul 09 22:01:41 2009 +0200
     7.3 @@ -51,8 +51,8 @@
     7.4  open FundefLib
     7.5  
     7.6  val term2_ord = prod_ord TermOrd.fast_term_ord TermOrd.fast_term_ord
     7.7 -structure Term2tab = TableFun(type key = term * term val ord = term2_ord);
     7.8 -structure Term3tab = TableFun(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
     7.9 +structure Term2tab = Table(type key = term * term val ord = term2_ord);
    7.10 +structure Term3tab = Table(type key = term * (term * term) val ord = prod_ord TermOrd.fast_term_ord term2_ord);
    7.11  
    7.12  (** Analyzing binary trees **)
    7.13  
     8.1 --- a/src/HOL/Tools/res_atp.ML	Thu Jul 09 17:34:59 2009 +0200
     8.2 +++ b/src/HOL/Tools/res_atp.ML	Thu Jul 09 22:01:41 2009 +0200
     8.3 @@ -152,7 +152,7 @@
     8.4  
     8.5  end;
     8.6  
     8.7 -structure CTtab = TableFun(type key = const_typ list val ord = dict_ord const_typ_ord);
     8.8 +structure CTtab = Table(type key = const_typ list val ord = dict_ord const_typ_ord);
     8.9  
    8.10  fun count_axiom_consts theory_const thy ((thm,_), tab) = 
    8.11    let fun count_const (a, T, tab) =
     9.1 --- a/src/Pure/Concurrent/task_queue.ML	Thu Jul 09 17:34:59 2009 +0200
     9.2 +++ b/src/Pure/Concurrent/task_queue.ML	Thu Jul 09 22:01:41 2009 +0200
     9.3 @@ -41,7 +41,7 @@
     9.4  fun str_of_task (Task (_, i)) = string_of_int i;
     9.5  
     9.6  fun task_ord (Task t1, Task t2) = prod_ord (rev_order o int_ord) int_ord (t1, t2);
     9.7 -structure Task_Graph = GraphFun(type key = task val ord = task_ord);
     9.8 +structure Task_Graph = Graph(type key = task val ord = task_ord);
     9.9  
    9.10  
    9.11  (* groups *)
    10.1 --- a/src/Pure/General/graph.ML	Thu Jul 09 17:34:59 2009 +0200
    10.2 +++ b/src/Pure/General/graph.ML	Thu Jul 09 22:01:41 2009 +0200
    10.3 @@ -52,7 +52,7 @@
    10.4    val extend: (key -> 'a * key list) -> key -> 'a T -> 'a T
    10.5  end;
    10.6  
    10.7 -functor GraphFun(Key: KEY): GRAPH =
    10.8 +functor Graph(Key: KEY): GRAPH =
    10.9  struct
   10.10  
   10.11  (* keys *)
   10.12 @@ -67,7 +67,7 @@
   10.13  
   10.14  (* tables and sets of keys *)
   10.15  
   10.16 -structure Table = TableFun(Key);
   10.17 +structure Table = Table(Key);
   10.18  type keys = unit Table.table;
   10.19  
   10.20  val empty_keys = Table.empty: keys;
   10.21 @@ -299,5 +299,5 @@
   10.22  
   10.23  end;
   10.24  
   10.25 -structure Graph = GraphFun(type key = string val ord = fast_string_ord);
   10.26 -structure IntGraph = GraphFun(type key = int val ord = int_ord);
   10.27 +structure Graph = Graph(type key = string val ord = fast_string_ord);
   10.28 +structure IntGraph = Graph(type key = int val ord = int_ord);
    11.1 --- a/src/Pure/General/table.ML	Thu Jul 09 17:34:59 2009 +0200
    11.2 +++ b/src/Pure/General/table.ML	Thu Jul 09 22:01:41 2009 +0200
    11.3 @@ -58,7 +58,7 @@
    11.4      'a list table * 'a list table -> 'a list table                     (*exception DUP*)
    11.5  end;
    11.6  
    11.7 -functor TableFun(Key: KEY): TABLE =
    11.8 +functor Table(Key: KEY): TABLE =
    11.9  struct
   11.10  
   11.11  
   11.12 @@ -409,8 +409,8 @@
   11.13  
   11.14  end;
   11.15  
   11.16 -structure Inttab = TableFun(type key = int val ord = int_ord);
   11.17 -structure Symtab = TableFun(type key = string val ord = fast_string_ord);
   11.18 -structure Symreltab = TableFun(type key = string * string
   11.19 +structure Inttab = Table(type key = int val ord = int_ord);
   11.20 +structure Symtab = Table(type key = string val ord = fast_string_ord);
   11.21 +structure Symreltab = Table(type key = string * string
   11.22    val ord = prod_ord fast_string_ord fast_string_ord);
   11.23  
    12.1 --- a/src/Pure/Isar/code.ML	Thu Jul 09 17:34:59 2009 +0200
    12.2 +++ b/src/Pure/Isar/code.ML	Thu Jul 09 22:01:41 2009 +0200
    12.3 @@ -355,7 +355,7 @@
    12.4  (* data slots dependent on executable code *)
    12.5  
    12.6  (*private copy avoids potential conflict of table exceptions*)
    12.7 -structure Datatab = TableFun(type key = int val ord = int_ord);
    12.8 +structure Datatab = Table(type key = int val ord = int_ord);
    12.9  
   12.10  local
   12.11  
    13.1 --- a/src/Pure/context.ML	Thu Jul 09 17:34:59 2009 +0200
    13.2 +++ b/src/Pure/context.ML	Thu Jul 09 22:01:41 2009 +0200
    13.3 @@ -97,7 +97,7 @@
    13.4  (* data kinds and access methods *)
    13.5  
    13.6  (*private copy avoids potential conflict of table exceptions*)
    13.7 -structure Datatab = TableFun(type key = int val ord = int_ord);
    13.8 +structure Datatab = Table(type key = int val ord = int_ord);
    13.9  
   13.10  local
   13.11  
    14.1 --- a/src/Pure/more_thm.ML	Thu Jul 09 17:34:59 2009 +0200
    14.2 +++ b/src/Pure/more_thm.ML	Thu Jul 09 22:01:41 2009 +0200
    14.3 @@ -414,4 +414,4 @@
    14.4  
    14.5  val op aconvc = Thm.aconvc;
    14.6  
    14.7 -structure Thmtab = TableFun(type key = thm val ord = Thm.thm_ord);
    14.8 +structure Thmtab = Table(type key = thm val ord = Thm.thm_ord);
    15.1 --- a/src/Pure/term_ord.ML	Thu Jul 09 17:34:59 2009 +0200
    15.2 +++ b/src/Pure/term_ord.ML	Thu Jul 09 22:01:41 2009 +0200
    15.3 @@ -204,6 +204,6 @@
    15.4  
    15.5  end;
    15.6  
    15.7 -structure Vartab = TableFun(type key = indexname val ord = TermOrd.fast_indexname_ord);
    15.8 -structure Typtab = TableFun(type key = typ val ord = TermOrd.typ_ord);
    15.9 -structure Termtab = TableFun(type key = term val ord = TermOrd.fast_term_ord);
   15.10 +structure Vartab = Table(type key = indexname val ord = TermOrd.fast_indexname_ord);
   15.11 +structure Typtab = Table(type key = typ val ord = TermOrd.typ_ord);
   15.12 +structure Termtab = Table(type key = term val ord = TermOrd.fast_term_ord);
    16.1 --- a/src/Tools/Code/code_preproc.ML	Thu Jul 09 17:34:59 2009 +0200
    16.2 +++ b/src/Tools/Code/code_preproc.ML	Thu Jul 09 22:01:41 2009 +0200
    16.3 @@ -253,7 +253,7 @@
    16.4  type var = const * int;
    16.5  
    16.6  structure Vargraph =
    16.7 -  GraphFun(type key = var val ord = prod_ord const_ord int_ord);
    16.8 +  Graph(type key = var val ord = prod_ord const_ord int_ord);
    16.9  
   16.10  datatype styp = Tyco of string * styp list | Var of var | Free;
   16.11  
    17.1 --- a/src/Tools/Compute_Oracle/am_interpreter.ML	Thu Jul 09 17:34:59 2009 +0200
    17.2 +++ b/src/Tools/Compute_Oracle/am_interpreter.ML	Thu Jul 09 22:01:41 2009 +0200
    17.3 @@ -16,7 +16,7 @@
    17.4                   | CApp of closure * closure | CAbs of closure
    17.5                   | Closure of (closure list) * closure
    17.6  
    17.7 -structure prog_struct = TableFun(type key = int*int val ord = prod_ord int_ord int_ord);
    17.8 +structure prog_struct = Table(type key = int*int val ord = prod_ord int_ord int_ord);
    17.9  
   17.10  datatype program = Program of ((pattern * closure * (closure*closure) list) list) prog_struct.table
   17.11  
    18.1 --- a/src/Tools/Compute_Oracle/compute.ML	Thu Jul 09 17:34:59 2009 +0200
    18.2 +++ b/src/Tools/Compute_Oracle/compute.ML	Thu Jul 09 22:01:41 2009 +0200
    18.3 @@ -167,7 +167,7 @@
    18.4    | machine_of_prog (ProgHaskell _) = HASKELL
    18.5    | machine_of_prog (ProgSML _) = SML
    18.6  
    18.7 -structure Sorttab = TableFun(type key = sort val ord = TermOrd.sort_ord)
    18.8 +structure Sorttab = Table(type key = sort val ord = TermOrd.sort_ord)
    18.9  
   18.10  type naming = int -> string
   18.11  
    19.1 --- a/src/Tools/Compute_Oracle/linker.ML	Thu Jul 09 17:34:59 2009 +0200
    19.2 +++ b/src/Tools/Compute_Oracle/linker.ML	Thu Jul 09 22:01:41 2009 +0200
    19.3 @@ -54,8 +54,8 @@
    19.4  fun constant_modty_ord (Constant (x1,x2,_), Constant (y1,y2,_)) = (prod_ord bool_ord fast_string_ord) ((x1,x2), (y1,y2))
    19.5  
    19.6  
    19.7 -structure Consttab = TableFun(type key = constant val ord = constant_ord);
    19.8 -structure ConsttabModTy = TableFun(type key = constant val ord = constant_modty_ord);
    19.9 +structure Consttab = Table(type key = constant val ord = constant_ord);
   19.10 +structure ConsttabModTy = Table(type key = constant val ord = constant_modty_ord);
   19.11  
   19.12  fun typ_of_constant (Constant (_, _, ty)) = ty
   19.13  
   19.14 @@ -72,7 +72,7 @@
   19.15  fun subst_ord (A:Type.tyenv, B:Type.tyenv) =
   19.16      (list_ord (prod_ord TermOrd.fast_indexname_ord (prod_ord TermOrd.sort_ord TermOrd.typ_ord))) (Vartab.dest A, Vartab.dest B)
   19.17  
   19.18 -structure Substtab = TableFun(type key = Type.tyenv val ord = subst_ord);
   19.19 +structure Substtab = Table(type key = Type.tyenv val ord = subst_ord);
   19.20  
   19.21  fun substtab_union c = Substtab.fold Substtab.update c
   19.22  fun substtab_unions [] = Substtab.empty
   19.23 @@ -382,7 +382,7 @@
   19.24  
   19.25  fun cthm_ord (ComputeThm (h1, sh1, p1), ComputeThm (h2, sh2, p2)) = cthm_ord' (((h1,sh1), p1), ((h2, sh2), p2))
   19.26  
   19.27 -structure CThmtab = TableFun (type key = cthm val ord = cthm_ord)
   19.28 +structure CThmtab = Table(type key = cthm val ord = cthm_ord)
   19.29  
   19.30  fun remove_duplicates ths =
   19.31      let