# HG changeset patch
# User wenzelm
# Date 1257694241 -3600
# Node ID e31a85f92ce9a4a39cd50e686f25831bab41c7af
# Parent  24563731b9b2f3ef4e36bc8948a84e8b93b6fdc5
adapted Generic_Data, Proof_Data;
tuned;

diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Algebra/ringsimp.ML
--- a/src/HOL/Algebra/ringsimp.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Algebra/ringsimp.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -18,7 +18,7 @@
 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
   (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = ((string * term list) * thm list) list;
     (* Algebraic structures:
@@ -26,7 +26,7 @@
        identifier and operations identify the structure uniquely. *)
   val empty = [];
   val extend = I;
-  fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
+  val merge = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
 );
 
 fun print_structures ctxt =
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/NSA/transfer.ML
--- a/src/HOL/NSA/transfer.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/NSA/transfer.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -15,7 +15,7 @@
 structure Transfer: TRANSFER =
 struct
 
-structure TransferData = GenericDataFun
+structure TransferData = Generic_Data
 (
   type T = {
     intros: thm list,
@@ -25,15 +25,15 @@
   };
   val empty = {intros = [], unfolds = [], refolds = [], consts = []};
   val extend = I;
-  fun merge _
+  fun merge
     ({intros = intros1, unfolds = unfolds1,
       refolds = refolds1, consts = consts1},
      {intros = intros2, unfolds = unfolds2,
-      refolds = refolds2, consts = consts2}) =
+      refolds = refolds2, consts = consts2}) : T =
    {intros = Thm.merge_thms (intros1, intros2),
     unfolds = Thm.merge_thms (unfolds1, unfolds2),
     refolds = Thm.merge_thms (refolds1, refolds2),
-    consts = Library.merge (op =) (consts1, consts2)} : T;
+    consts = Library.merge (op =) (consts1, consts2)};
 );
 
 fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Nominal/nominal_thmdecls.ML
--- a/src/HOL/Nominal/nominal_thmdecls.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -25,12 +25,12 @@
 structure NominalThmDecls: NOMINAL_THMDECLS =
 struct
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = thm list
-  val empty = []:T
+  val empty = []
   val extend = I
-  fun merge _ (r1:T, r2:T) = Thm.merge_thms (r1, r2)
+  val merge = Thm.merge_thms
 )
 
 (* Exception for when a theorem does not conform with form of an equivariance lemma. *)
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Orderings.thy	Sun Nov 08 16:30:41 2009 +0100
@@ -302,7 +302,7 @@
 fun struct_eq ((s1: string, ts1), (s2, ts2)) =
   (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = ((string * term list) * Order_Tac.less_arith) list;
     (* Order structures:
@@ -311,7 +311,7 @@
        identifier and operations identify the structure uniquely. *)
   val empty = [];
   val extend = I;
-  fun merge _ = AList.join struct_eq (K fst);
+  fun merge data = AList.join struct_eq (K fst) data;
 );
 
 fun print_structures ctxt =
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/SMT/Tools/smt_solver.ML
--- a/src/HOL/SMT/Tools/smt_solver.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -223,12 +223,13 @@
 
 (* selected solver *)
 
-structure SelectedSolver = GenericDataFun
+structure SelectedSolver = Generic_Data
 (
   type T = serial * string
   val empty = (serial (), no_solver)
   val extend = I
-  fun merge _ (sl1 as (s1, _), sl2 as (s2, _)) = if s1 > s2 then sl1 else sl2
+  fun merge (sl1 as (s1, _), sl2 as (s2, _)) =
+    if s1 > s2 then sl1 else sl2   (* FIXME depends on accidental load order !?! *)
 )
 
 val solver_name_of = snd o SelectedSolver.get
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/SMT/Tools/z3_proof_rules.ML
--- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -1091,12 +1091,12 @@
   val name = "z3_rewrite"
   val descr = "Z3 rewrite rules used in proof reconstruction"
 
-  structure Data = GenericDataFun
+  structure Data = Generic_Data
   (
     type T = thm Net.net
     val empty = Net.empty
     val extend = I
-    fun merge _ = Net.merge Thm.eq_thm_prop
+    val merge = Net.merge Thm.eq_thm_prop
   )
   val get = Data.get o Context.Proof
 
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Statespace/state_fun.ML
--- a/src/HOL/Statespace/state_fun.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Statespace/state_fun.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -93,20 +93,16 @@
 
 val ex_lookup_ss = HOL_ss addsimps @{thms StateFun.ex_id};
 
-structure StateFunArgs =
-struct
-  type T = (simpset * simpset * bool); 
+
+structure StateFunData = Generic_Data
+(
+  type T = simpset * simpset * bool;
            (* lookup simpset, ex_lookup simpset, are simprocs installed *)
   val empty = (empty_ss, empty_ss, false);
   val extend = I;
-  fun merge pp ((ss1,ex_ss1,b1),(ss2,ex_ss2,b2)) = 
-               (merge_ss (ss1,ss2)
-               ,merge_ss (ex_ss1,ex_ss2)
-               ,b1 orelse b2);
-end;
-
-
-structure StateFunData = GenericDataFun(StateFunArgs);
+  fun merge ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) =
+    (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
+);
 
 val init_state_fun_data =
   Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Statespace/state_space.ML
--- a/src/HOL/Statespace/state_space.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Statespace/state_space.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -106,19 +106,18 @@
   silent: bool
  };
 
-structure NameSpaceArgs =
-struct
+structure NameSpaceData = Generic_Data
+(
   type T = namespace_info;
   val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false};
   val extend = I;
-  fun merge pp ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
-                {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) =
-                {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
-                 distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
-                 silent = silent1 andalso silent2}
-end;
-
-structure NameSpaceData = GenericDataFun(NameSpaceArgs);
+  fun merge
+    ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
+      {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T =
+    {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
+     distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
+     silent = silent1 andalso silent2}
+);
 
 fun make_namespace_data declinfo distinctthm silent =
      {declinfo=declinfo,distinctthm=distinctthm,silent=silent};
@@ -172,17 +171,13 @@
   types: typ list (* range types of state space *)
  };
 
-structure StateSpaceArgs =
-struct
-  val name = "HOL/StateSpace";
+structure StateSpaceData = Generic_Data
+(
   type T = statespace_info Symtab.table;
   val empty = Symtab.empty;
   val extend = I;
-
-  fun merge pp (nt1,nt2) = Symtab.merge (K true) (nt1, nt2);
-end;
-
-structure StateSpaceData = GenericDataFun(StateSpaceArgs);
+  fun merge data : T = Symtab.merge (K true) data;
+);
 
 fun add_statespace name args parents components types ctxt =
      StateSpaceData.put
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/Function/context_tree.ML
--- a/src/HOL/Tools/Function/context_tree.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/Function/context_tree.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -44,12 +44,12 @@
 open Function_Common
 open Function_Lib
 
-structure FunctionCongs = GenericDataFun
+structure FunctionCongs = Generic_Data
 (
   type T = thm list
   val empty = []
   val extend = I
-  fun merge _ = Thm.merge_thms
+  val merge = Thm.merge_thms
 );
 
 val get_function_congs = FunctionCongs.get o Context.Proof
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/Function/function_common.ML
--- a/src/HOL/Tools/Function/function_common.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/Function/function_common.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -27,12 +27,12 @@
 
 (* Termination rules *)
 
-structure TerminationRule = GenericDataFun
+structure TerminationRule = Generic_Data
 (
   type T = thm list
   val empty = []
   val extend = I
-  fun merge _ = Thm.merge_thms
+  val merge = Thm.merge_thms
 );
 
 val get_termination_rules = TerminationRule.get
@@ -90,13 +90,12 @@
                       defname = name defname }
     end
 
-structure FunctionData = GenericDataFun
+structure FunctionData = Generic_Data
 (
   type T = (term * function_context_data) Item_Net.T;
   val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
-  val copy = I;
   val extend = I;
-  fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
+  fun merge tabs : T = Item_Net.merge tabs;
 );
 
 val get_function = FunctionData.get o Context.Proof;
@@ -152,12 +151,12 @@
 
 (* Default Termination Prover *)
 
-structure TerminationProver = GenericDataFun
+structure TerminationProver = Generic_Data
 (
   type T = Proof.context -> Proof.method
   val empty = (fn _ => error "Termination prover not configured")
   val extend = I
-  fun merge _ (a,b) = b (* FIXME *)
+  fun merge (a, b) = b  (* FIXME ? *)
 );
 
 val set_termination_prover = TerminationProver.put
@@ -310,12 +309,12 @@
       (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
     end
 
-structure Preprocessor = GenericDataFun
+structure Preprocessor = Generic_Data
 (
   type T = preproc
   val empty : T = empty_preproc check_defs
   val extend = I
-  fun merge _ (a, _) = a
+  fun merge (a, _) = a
 );
 
 val get_preproc = Preprocessor.get o Context.Proof
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/Groebner_Basis/normalizer_data.ML
--- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -40,12 +40,12 @@
 val eq_key = Thm.eq_thm;
 fun eq_data arg = eq_fst eq_key arg;
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = simpset * (thm * entry) list;
   val empty = (HOL_basic_ss, []);
   val extend = I;
-  fun merge _ ((ss, e), (ss', e')) =
+  fun merge ((ss, e), (ss', e')) : T =
     (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
 );
 
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -2450,7 +2450,7 @@
   (*FIXME name discrepancy in attribs and ML code*)
   (*FIXME intros should be better named intro*)
 
-(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
+(* TODO: make TheoryDataFun to Generic_Data & remove duplication of local theory and theory *)
 fun generic_code_pred prep_const options raw_const lthy =
   let
     val thy = ProofContext.theory_of lthy
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/Qelim/cooper_data.ML
--- a/src/HOL/Tools/Qelim/cooper_data.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/Qelim/cooper_data.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -44,12 +44,12 @@
    @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
    @{term "True"}, @{term "False"}];
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
-  type T = simpset * (term list);
+  type T = simpset * term list;
   val empty = (start_ss, allowed_consts);
   val extend  = I;
-  fun merge _ ((ss1, ts1), (ss2, ts2)) =
+  fun merge ((ss1, ts1), (ss2, ts2)) =
     (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
 );
 
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
--- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -38,12 +38,12 @@
 val eq_key = Thm.eq_thm;
 fun eq_data arg = eq_fst eq_key arg;
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = (thm * entry) list;
   val empty = [];
   val extend = I;
-  fun merge _ = AList.merge eq_key (K true);
+  fun merge data : T = AList.merge eq_key (K true) data;
 );
 
 val get = Data.get o Context.Proof;
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/Qelim/langford_data.ML
--- a/src/HOL/Tools/Qelim/langford_data.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/Qelim/langford_data.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -17,12 +17,13 @@
 val eq_key = Thm.eq_thm;
 fun eq_data arg = eq_fst eq_key arg;
 
-structure Data = GenericDataFun
-( type T = simpset * (thm * entry) list;
+structure Data = Generic_Data
+(
+  type T = simpset * (thm * entry) list;
   val empty = (HOL_basic_ss, []);
   val extend = I;
-  fun merge _ ((ss1,es1), (ss2,es2)) = 
-       (merge_ss (ss1,ss2), AList.merge eq_key (K true) (es1,es2));;
+  fun merge ((ss1, es1), (ss2, es2)) : T =
+    (merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2));
 );
 
 val get = Data.get o Context.Proof;
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -136,12 +136,12 @@
 type inductive_info =
   {names: string list, coind: bool} * inductive_result;
 
-structure InductiveData = GenericDataFun
+structure InductiveData = Generic_Data
 (
   type T = inductive_info Symtab.table * thm list;
   val empty = (Symtab.empty, []);
   val extend = I;
-  fun merge _ ((tab1, monos1), (tab2, monos2)) =
+  fun merge ((tab1, monos1), (tab2, monos2)) : T =
     (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2));
 );
 
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/inductive_set.ML
--- a/src/HOL/Tools/inductive_set.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/inductive_set.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -152,7 +152,7 @@
 (* where s and p are parameters                            *)
 (***********************************************************)
 
-structure PredSetConvData = GenericDataFun
+structure PredSetConvData = Generic_Data
 (
   type T =
     {(* rules for converting predicates to sets *)
@@ -166,7 +166,7 @@
   val empty = {to_set_simps = [], to_pred_simps = [],
     set_arities = Symtab.empty, pred_arities = Symtab.empty};
   val extend = I;
-  fun merge _
+  fun merge
     ({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1,
       set_arities = set_arities1, pred_arities = pred_arities1},
      {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/lin_arith.ML
--- a/src/HOL/Tools/lin_arith.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/lin_arith.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -72,14 +72,14 @@
 
 (* arith context data *)
 
-structure Lin_Arith_Data = GenericDataFun
+structure Lin_Arith_Data = Generic_Data
 (
   type T = {splits: thm list,
             inj_consts: (string * typ) list,
             discrete: string list};
   val empty = {splits = [], inj_consts = [], discrete = []};
   val extend = I;
-  fun merge _
+  fun merge
    ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
     {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T =
    {splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/recdef.ML
--- a/src/HOL/Tools/recdef.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/recdef.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -115,7 +115,7 @@
 
 (* proof data *)
 
-structure LocalRecdefData = ProofDataFun
+structure LocalRecdefData = Proof_Data
 (
   type T = hints;
   val init = get_global_hints;
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/res_blacklist.ML
--- a/src/HOL/Tools/res_blacklist.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/res_blacklist.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -19,12 +19,12 @@
 structure Res_Blacklist: RES_BLACKLIST =
 struct
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = thm Termtab.table;
   val empty = Termtab.empty;
   val extend = I;
-  fun merge _ tabs = Termtab.merge (K true) tabs;
+  fun merge tabs = Termtab.merge (K true) tabs;
 );
 
 fun blacklisted ctxt th =
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOL/Tools/transfer.ML
--- a/src/HOL/Tools/transfer.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOL/Tools/transfer.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -25,12 +25,12 @@
 
 type data = simpset * (thm * entry) list;
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = data;
   val empty = (HOL_ss, []);
   val extend  = I;
-  fun merge _ ((ss1, e1), (ss2, e2)) =
+  fun merge ((ss1, e1), (ss2, e2)) : T =
     (merge_ss (ss1, ss2), AList.join Thm.eq_thm (K merge_entry) (e1, e2));
 );
 
diff -r 24563731b9b2 -r e31a85f92ce9 src/HOLCF/Tools/fixrec.ML
--- a/src/HOLCF/Tools/fixrec.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/HOLCF/Tools/fixrec.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -160,12 +160,12 @@
 (************* fixed-point definitions and unfolding theorems ************)
 (*************************************************************************)
 
-structure FixrecUnfoldData = GenericDataFun (
+structure FixrecUnfoldData = Generic_Data
+(
   type T = thm Symtab.table;
   val empty = Symtab.empty;
-  val copy = I;
   val extend = I;
-  fun merge _ = Symtab.merge (K true);
+  fun merge data : T = Symtab.merge (K true) data;
 );
 
 local
@@ -363,16 +363,16 @@
 (********************** Proving associated theorems **********************)
 (*************************************************************************)
 
-structure FixrecSimpData = GenericDataFun (
+structure FixrecSimpData = Generic_Data
+(
   type T = simpset;
   val empty =
     HOL_basic_ss
       addsimps simp_thms
       addsimps [@{thm beta_cfun}]
       addsimprocs [@{simproc cont_proc}];
-  val copy = I;
   val extend = I;
-  fun merge _ = merge_ss;
+  val merge = merge_ss;
 );
 
 fun fixrec_simp_tac ctxt =
diff -r 24563731b9b2 -r e31a85f92ce9 src/Provers/Arith/fast_lin_arith.ML
--- a/src/Provers/Arith/fast_lin_arith.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -109,7 +109,7 @@
 
 fun no_number_of _ _ _ = raise CTERM ("number_of", [])
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T =
    {add_mono_thms: thm list,
@@ -124,7 +124,7 @@
                lessD = [], neqE = [], simpset = Simplifier.empty_ss,
                number_of = (serial (), no_number_of) } : T;
   val extend = I;
-  fun merge _
+  fun merge
     ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
       lessD = lessD1, neqE=neqE1, simpset = simpset1,
       number_of = (number_of1 as (s1, _))},
@@ -137,6 +137,7 @@
      lessD = Thm.merge_thms (lessD1, lessD2),
      neqE = Thm.merge_thms (neqE1, neqE2),
      simpset = Simplifier.merge_ss (simpset1, simpset2),
+     (* FIXME depends on accidental load order !?! *)
      number_of = if s1 > s2 then number_of1 else number_of2};
 );
 
diff -r 24563731b9b2 -r e31a85f92ce9 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Provers/classical.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -868,7 +868,7 @@
 
 (* local clasets *)
 
-structure LocalClaset = ProofDataFun
+structure LocalClaset = Proof_Data
 (
   type T = claset;
   val init = get_global_claset;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/calculation.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -27,13 +27,12 @@
 
 (** calculation data **)
 
-structure CalculationData = GenericDataFun
+structure CalculationData = Generic_Data
 (
   type T = (thm Item_Net.T * thm list) * (thm list * int) option;
   val empty = ((Thm.elim_rules, []), NONE);
   val extend = I;
-
-  fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
+  fun merge (((trans1, sym1), _), ((trans2, sym2), _)) =
     ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
 );
 
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/class_target.ML
--- a/src/Pure/Isar/class_target.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/class_target.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -398,7 +398,7 @@
     (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
 }
 
-structure Instantiation = ProofDataFun
+structure Instantiation = Proof_Data
 (
   type T = instantiation
   fun init _ = Instantiation { arities = ([], [], []), params = [] };
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/code.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -794,12 +794,12 @@
 structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS =
 struct
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = thm list;
   val empty = [];
   val extend = I;
-  fun merge _ = Thm.merge_thms;
+  val merge = Thm.merge_thms;
 );
 
 val get = Data.get o Context.Proof;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/context_rules.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -89,13 +89,13 @@
     else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
   end;
 
-structure Rules = GenericDataFun
+structure Rules = Generic_Data
 (
   type T = rules;
   val empty = make_rules ~1 [] empty_netpairs ([], []);
   val extend = I;
-
-  fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
+  fun merge
+    (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
       Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
     let
       val wrappers =
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/local_defs.ML
--- a/src/Pure/Isar/local_defs.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/local_defs.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -186,12 +186,12 @@
 
 (* transformation rules *)
 
-structure Rules = GenericDataFun
+structure Rules = Generic_Data
 (
   type T = thm list;
-  val empty = []
+  val empty = [];
   val extend = I;
-  fun merge _ = Thm.merge_thms;
+  val merge = Thm.merge_thms;
 );
 
 fun print_rules ctxt =
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/local_theory.ML
--- a/src/Pure/Isar/local_theory.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/local_theory.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -85,7 +85,7 @@
 
 (* context data *)
 
-structure Data = ProofDataFun
+structure Data = Proof_Data
 (
   type T = lthy option;
   fun init _ = NONE;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -188,12 +188,12 @@
 
 datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
 
-structure Identifiers = GenericDataFun
+structure Identifiers = Generic_Data
 (
   type T = (string * term list) list delayed;
   val empty = Ready [];
   val extend = I;
-  fun merge _ = ToDo;
+  val merge = ToDo;
 );
 
 fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
@@ -569,12 +569,12 @@
 
 (* Storage for witnesses, intro and unfold rules *)
 
-structure Thms = GenericDataFun
+structure Thms = Generic_Data
 (
   type T = thm list * thm list * thm list;
   val empty = ([], [], []);
   val extend = I;
-  fun merge _ ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
+  fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
    (Thm.merge_thms (witnesses1, witnesses2),
     Thm.merge_thms (intros1, intros2),
     Thm.merge_thms (unfolds1, unfolds2));
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/method.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -270,7 +270,7 @@
 
 (* ML tactics *)
 
-structure TacticData = ProofDataFun
+structure TacticData = Proof_Data
 (
   type T = thm list -> tactic;
   fun init _ = undefined;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/overloading.ML
--- a/src/Pure/Isar/overloading.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/overloading.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -30,7 +30,8 @@
   ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) *
     (term * term) list)) * bool);
 
-structure ImprovableSyntax = ProofDataFun(
+structure ImprovableSyntax = Proof_Data
+(
   type T = {
     primary_constraints: (string * typ) list,
     secondary_constraints: (string * typ) list,
@@ -119,7 +120,7 @@
 
 (* bookkeeping *)
 
-structure OverloadingData = ProofDataFun
+structure OverloadingData = Proof_Data
 (
   type T = ((string * typ) * (string * bool)) list;
   fun init _ = [];
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -177,7 +177,7 @@
 
 val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
 
-structure ContextData = ProofDataFun
+structure ContextData = Proof_Data
 (
   type T = ctxt;
   fun init thy =
@@ -515,7 +515,7 @@
 
 local
 
-structure Allow_Dummies = ProofDataFun(type T = bool fun init _ = false);
+structure Allow_Dummies = Proof_Data(type T = bool fun init _ = false);
 
 fun check_dummies ctxt t =
   if Allow_Dummies.get ctxt then t
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/spec_rules.ML
--- a/src/Pure/Isar/spec_rules.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/spec_rules.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -24,7 +24,7 @@
 datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive;
 type spec = rough_classification * (term list * thm list);
 
-structure Rules = GenericDataFun
+structure Rules = Generic_Data
 (
   type T = spec Item_Net.T;
   val empty : T =
@@ -35,7 +35,7 @@
         eq_list Thm.eq_thm_prop (ths1, ths2))
       (#1 o #2);
   val extend = I;
-  fun merge _ = Item_Net.merge;
+  fun merge data = Item_Net.merge data;
 );
 
 val get = Item_Net.content o Rules.get o Context.Proof;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/specification.ML
--- a/src/Pure/Isar/specification.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/specification.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -333,12 +333,12 @@
                 [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
       in ((prems, stmt, SOME facts), goal_ctxt) end);
 
-structure TheoremHook = GenericDataFun
+structure TheoremHook = Generic_Data
 (
   type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
   val empty = [];
   val extend = I;
-  fun merge _ hooks : T = Library.merge (eq_snd op =) hooks;
+  fun merge hooks : T = Library.merge (eq_snd op =) hooks;
 );
 
 fun gen_theorem prep_att prep_stmt
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/theory_target.ML
--- a/src/Pure/Isar/theory_target.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/theory_target.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -34,7 +34,7 @@
 
 val global_target = make_target "" false false ([], [], []) [];
 
-structure Data = ProofDataFun
+structure Data = Proof_Data
 (
   type T = target;
   fun init _ = global_target;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -631,7 +631,7 @@
 
 (* excursion of units, consisting of commands with proof *)
 
-structure States = ProofDataFun
+structure States = Proof_Data
 (
   type T = state list future option;
   fun init _ = NONE;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/ML/ml_antiquote.ML
--- a/src/Pure/ML/ml_antiquote.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/ML/ml_antiquote.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -20,7 +20,7 @@
 
 (* ML names *)
 
-structure NamesData = ProofDataFun
+structure NamesData = Proof_Data
 (
   type T = Name.context;
   fun init _ = ML_Syntax.reserved;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/ML/ml_env.ML
--- a/src/Pure/ML/ml_env.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/ML/ml_env.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -16,7 +16,7 @@
 
 (* context data *)
 
-structure Env = GenericDataFun
+structure Env = Generic_Data
 (
   type T =
     ML_Name_Space.valueVal Symtab.table *
@@ -27,7 +27,7 @@
     ML_Name_Space.functorVal Symtab.table;
   val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
   val extend = I;
-  fun merge _
+  fun merge
    ((val1, type1, fixity1, structure1, signature1, functor1),
     (val2, type2, fixity2, structure2, signature2, functor2)) : T =
     (Symtab.merge (K true) (val1, val2),
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/ML/ml_thms.ML
--- a/src/Pure/ML/ml_thms.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/ML/ml_thms.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -15,7 +15,7 @@
 
 (* auxiliary facts table *)
 
-structure AuxFacts = ProofDataFun
+structure AuxFacts = Proof_Data
 (
   type T = thm list Inttab.table;
   fun init _ = Inttab.empty;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -741,14 +741,14 @@
 type key = int * bool;
 type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
 
-structure Checks = GenericDataFun
+structure Checks = Generic_Data
 (
   type T =
     ((key * ((string * typ check) * stamp) list) list *
      (key * ((string * term check) * stamp) list) list);
   val empty = ([], []);
   val extend = I;
-  fun merge _ ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
+  fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
     (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
      AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
 );
@@ -877,7 +877,7 @@
 
 (* global pretty printing *)
 
-structure PrettyGlobal = ProofDataFun(type T = bool fun init _ = false);
+structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
 val is_pretty_global = PrettyGlobal.get;
 val set_pretty_global = PrettyGlobal.put;
 val init_pretty_global = set_pretty_global true o ProofContext.init;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/Tools/named_thms.ML
--- a/src/Pure/Tools/named_thms.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/Tools/named_thms.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -17,12 +17,12 @@
 functor Named_Thms(val name: string val description: string): NAMED_THMS =
 struct
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
   type T = thm Item_Net.T;
   val empty = Thm.full_rules;
   val extend = I;
-  fun merge _ = Item_Net.merge;
+  val merge = Item_Net.merge;
 );
 
 val content = Item_Net.content o Data.get;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/assumption.ML
--- a/src/Pure/assumption.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/assumption.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -60,7 +60,7 @@
 
 fun make_data (assms, prems) = Data {assms = assms, prems = prems};
 
-structure Data = ProofDataFun
+structure Data = Proof_Data
 (
   type T = data;
   fun init _ = make_data ([], []);
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/config.ML
--- a/src/Pure/config.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/config.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -90,12 +90,12 @@
 
 (* context information *)
 
-structure Value = GenericDataFun
+structure Value = Generic_Data
 (
   type T = value Inttab.table;
   val empty = Inttab.empty;
   val extend = I;
-  fun merge _ = Inttab.merge (K true);
+  fun merge data = Inttab.merge (K true) data;
 );
 
 fun declare global name default =
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/context_position.ML
--- a/src/Pure/context_position.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/context_position.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -15,7 +15,7 @@
 structure Context_Position: CONTEXT_POSITION =
 struct
 
-structure Data = ProofDataFun
+structure Data = Proof_Data
 (
   type T = bool;
   fun init _ = true;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/simplifier.ML
--- a/src/Pure/simplifier.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/simplifier.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -99,12 +99,12 @@
 
 (** simpset data **)
 
-structure SimpsetData = GenericDataFun
+structure SimpsetData = Generic_Data
 (
   type T = simpset;
   val empty = empty_ss;
   fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
-  fun merge _ = merge_ss;
+  val merge = merge_ss;
 );
 
 val get_ss = SimpsetData.get;
@@ -145,12 +145,12 @@
 
 (* data *)
 
-structure Simprocs = GenericDataFun
+structure Simprocs = Generic_Data
 (
   type T = simproc Name_Space.table;
   val empty : T = Name_Space.empty_table "simproc";
   val extend = I;
-  fun merge _ simprocs = Name_Space.merge_tables simprocs;
+  fun merge simprocs = Name_Space.merge_tables simprocs;
 );
 
 
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/type.ML
--- a/src/Pure/type.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/type.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -147,7 +147,7 @@
 val mode_syntax = Mode {normalize = true, logical = false};
 val mode_abbrev = Mode {normalize = false, logical = false};
 
-structure Mode = ProofDataFun
+structure Mode = Proof_Data
 (
   type T = mode;
   fun init _ = mode_default;
diff -r 24563731b9b2 -r e31a85f92ce9 src/Pure/variable.ML
--- a/src/Pure/variable.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Pure/variable.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -86,7 +86,7 @@
   Data {is_body = is_body, names = names, consts = consts, fixes = fixes, binds = binds,
     type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
 
-structure Data = ProofDataFun
+structure Data = Proof_Data
 (
   type T = data;
   fun init _ =
diff -r 24563731b9b2 -r e31a85f92ce9 src/Tools/Code/code_ml.ML
--- a/src/Tools/Code/code_ml.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Tools/Code/code_ml.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -947,7 +947,7 @@
 
 local
 
-structure CodeAntiqData = ProofDataFun
+structure CodeAntiqData = Proof_Data
 (
   type T = (string list * string list) * (bool * (string
     * (string * ((string * string) list * (string * string) list)) lazy));
diff -r 24563731b9b2 -r e31a85f92ce9 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/Tools/induct.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -130,7 +130,7 @@
 
 (* context data *)
 
-structure InductData = GenericDataFun
+structure InductData = Generic_Data
 (
   type T = (rules * rules) * (rules * rules) * (rules * rules);
   val empty =
@@ -138,7 +138,7 @@
      (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
      (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
   val extend = I;
-  fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
+  fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
       ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
     ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
       (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
diff -r 24563731b9b2 -r e31a85f92ce9 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Sun Nov 08 16:28:18 2009 +0100
+++ b/src/ZF/Tools/typechk.ML	Sun Nov 08 16:30:41 2009 +0100
@@ -43,15 +43,13 @@
 
 (* generic data *)
 
-structure Data = GenericDataFun
+structure Data = Generic_Data
 (
-  type T = tcset
+  type T = tcset;
   val empty = TC {rules = [], net = Net.empty};
   val extend = I;
-
-  fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
-    TC {rules = Thm.merge_thms (rules, rules'),
-        net = Net.merge Thm.eq_thm_prop (net, net')};
+  fun merge (TC {rules, net}, TC {rules = rules', net = net'}) =
+    TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')};
 );
 
 val TC_add = Thm.declaration_attribute (Data.map o add_rule);