adapted Generic_Data, Proof_Data;
authorwenzelm
Sun Nov 08 16:30:41 2009 +0100 (2009-11-08 ago)
changeset 33519e31a85f92ce9
parent 33518 24563731b9b2
child 33520 b2cb4da715f7
adapted Generic_Data, Proof_Data;
tuned;
src/HOL/Algebra/ringsimp.ML
src/HOL/NSA/transfer.ML
src/HOL/Nominal/nominal_thmdecls.ML
src/HOL/Orderings.thy
src/HOL/SMT/Tools/smt_solver.ML
src/HOL/SMT/Tools/z3_proof_rules.ML
src/HOL/Statespace/state_fun.ML
src/HOL/Statespace/state_space.ML
src/HOL/Tools/Function/context_tree.ML
src/HOL/Tools/Function/function_common.ML
src/HOL/Tools/Groebner_Basis/normalizer_data.ML
src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML
src/HOL/Tools/Qelim/cooper_data.ML
src/HOL/Tools/Qelim/ferrante_rackoff_data.ML
src/HOL/Tools/Qelim/langford_data.ML
src/HOL/Tools/inductive.ML
src/HOL/Tools/inductive_set.ML
src/HOL/Tools/lin_arith.ML
src/HOL/Tools/recdef.ML
src/HOL/Tools/res_blacklist.ML
src/HOL/Tools/transfer.ML
src/HOLCF/Tools/fixrec.ML
src/Provers/Arith/fast_lin_arith.ML
src/Provers/classical.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/class_target.ML
src/Pure/Isar/code.ML
src/Pure/Isar/context_rules.ML
src/Pure/Isar/local_defs.ML
src/Pure/Isar/local_theory.ML
src/Pure/Isar/locale.ML
src/Pure/Isar/method.ML
src/Pure/Isar/overloading.ML
src/Pure/Isar/proof_context.ML
src/Pure/Isar/spec_rules.ML
src/Pure/Isar/specification.ML
src/Pure/Isar/theory_target.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML/ml_antiquote.ML
src/Pure/ML/ml_env.ML
src/Pure/ML/ml_thms.ML
src/Pure/Syntax/syntax.ML
src/Pure/Tools/named_thms.ML
src/Pure/assumption.ML
src/Pure/config.ML
src/Pure/context_position.ML
src/Pure/simplifier.ML
src/Pure/type.ML
src/Pure/variable.ML
src/Tools/Code/code_ml.ML
src/Tools/induct.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Algebra/ringsimp.ML	Sun Nov 08 16:28:18 2009 +0100
     1.2 +++ b/src/HOL/Algebra/ringsimp.ML	Sun Nov 08 16:30:41 2009 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4  fun struct_eq ((s1: string, ts1), (s2, ts2)) =
     1.5    (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
     1.6  
     1.7 -structure Data = GenericDataFun
     1.8 +structure Data = Generic_Data
     1.9  (
    1.10    type T = ((string * term list) * thm list) list;
    1.11      (* Algebraic structures:
    1.12 @@ -26,7 +26,7 @@
    1.13         identifier and operations identify the structure uniquely. *)
    1.14    val empty = [];
    1.15    val extend = I;
    1.16 -  fun merge _ = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
    1.17 +  val merge = AList.join struct_eq (K (Library.merge Thm.eq_thm_prop));
    1.18  );
    1.19  
    1.20  fun print_structures ctxt =
     2.1 --- a/src/HOL/NSA/transfer.ML	Sun Nov 08 16:28:18 2009 +0100
     2.2 +++ b/src/HOL/NSA/transfer.ML	Sun Nov 08 16:30:41 2009 +0100
     2.3 @@ -15,7 +15,7 @@
     2.4  structure Transfer: TRANSFER =
     2.5  struct
     2.6  
     2.7 -structure TransferData = GenericDataFun
     2.8 +structure TransferData = Generic_Data
     2.9  (
    2.10    type T = {
    2.11      intros: thm list,
    2.12 @@ -25,15 +25,15 @@
    2.13    };
    2.14    val empty = {intros = [], unfolds = [], refolds = [], consts = []};
    2.15    val extend = I;
    2.16 -  fun merge _
    2.17 +  fun merge
    2.18      ({intros = intros1, unfolds = unfolds1,
    2.19        refolds = refolds1, consts = consts1},
    2.20       {intros = intros2, unfolds = unfolds2,
    2.21 -      refolds = refolds2, consts = consts2}) =
    2.22 +      refolds = refolds2, consts = consts2}) : T =
    2.23     {intros = Thm.merge_thms (intros1, intros2),
    2.24      unfolds = Thm.merge_thms (unfolds1, unfolds2),
    2.25      refolds = Thm.merge_thms (refolds1, refolds2),
    2.26 -    consts = Library.merge (op =) (consts1, consts2)} : T;
    2.27 +    consts = Library.merge (op =) (consts1, consts2)};
    2.28  );
    2.29  
    2.30  fun unstar_typ (Type ("StarDef.star",[t])) = unstar_typ t
     3.1 --- a/src/HOL/Nominal/nominal_thmdecls.ML	Sun Nov 08 16:28:18 2009 +0100
     3.2 +++ b/src/HOL/Nominal/nominal_thmdecls.ML	Sun Nov 08 16:30:41 2009 +0100
     3.3 @@ -25,12 +25,12 @@
     3.4  structure NominalThmDecls: NOMINAL_THMDECLS =
     3.5  struct
     3.6  
     3.7 -structure Data = GenericDataFun
     3.8 +structure Data = Generic_Data
     3.9  (
    3.10    type T = thm list
    3.11 -  val empty = []:T
    3.12 +  val empty = []
    3.13    val extend = I
    3.14 -  fun merge _ (r1:T, r2:T) = Thm.merge_thms (r1, r2)
    3.15 +  val merge = Thm.merge_thms
    3.16  )
    3.17  
    3.18  (* Exception for when a theorem does not conform with form of an equivariance lemma. *)
     4.1 --- a/src/HOL/Orderings.thy	Sun Nov 08 16:28:18 2009 +0100
     4.2 +++ b/src/HOL/Orderings.thy	Sun Nov 08 16:30:41 2009 +0100
     4.3 @@ -302,7 +302,7 @@
     4.4  fun struct_eq ((s1: string, ts1), (s2, ts2)) =
     4.5    (s1 = s2) andalso eq_list (op aconv) (ts1, ts2);
     4.6  
     4.7 -structure Data = GenericDataFun
     4.8 +structure Data = Generic_Data
     4.9  (
    4.10    type T = ((string * term list) * Order_Tac.less_arith) list;
    4.11      (* Order structures:
    4.12 @@ -311,7 +311,7 @@
    4.13         identifier and operations identify the structure uniquely. *)
    4.14    val empty = [];
    4.15    val extend = I;
    4.16 -  fun merge _ = AList.join struct_eq (K fst);
    4.17 +  fun merge data = AList.join struct_eq (K fst) data;
    4.18  );
    4.19  
    4.20  fun print_structures ctxt =
     5.1 --- a/src/HOL/SMT/Tools/smt_solver.ML	Sun Nov 08 16:28:18 2009 +0100
     5.2 +++ b/src/HOL/SMT/Tools/smt_solver.ML	Sun Nov 08 16:30:41 2009 +0100
     5.3 @@ -223,12 +223,13 @@
     5.4  
     5.5  (* selected solver *)
     5.6  
     5.7 -structure SelectedSolver = GenericDataFun
     5.8 +structure SelectedSolver = Generic_Data
     5.9  (
    5.10    type T = serial * string
    5.11    val empty = (serial (), no_solver)
    5.12    val extend = I
    5.13 -  fun merge _ (sl1 as (s1, _), sl2 as (s2, _)) = if s1 > s2 then sl1 else sl2
    5.14 +  fun merge (sl1 as (s1, _), sl2 as (s2, _)) =
    5.15 +    if s1 > s2 then sl1 else sl2   (* FIXME depends on accidental load order !?! *)
    5.16  )
    5.17  
    5.18  val solver_name_of = snd o SelectedSolver.get
     6.1 --- a/src/HOL/SMT/Tools/z3_proof_rules.ML	Sun Nov 08 16:28:18 2009 +0100
     6.2 +++ b/src/HOL/SMT/Tools/z3_proof_rules.ML	Sun Nov 08 16:30:41 2009 +0100
     6.3 @@ -1091,12 +1091,12 @@
     6.4    val name = "z3_rewrite"
     6.5    val descr = "Z3 rewrite rules used in proof reconstruction"
     6.6  
     6.7 -  structure Data = GenericDataFun
     6.8 +  structure Data = Generic_Data
     6.9    (
    6.10      type T = thm Net.net
    6.11      val empty = Net.empty
    6.12      val extend = I
    6.13 -    fun merge _ = Net.merge Thm.eq_thm_prop
    6.14 +    val merge = Net.merge Thm.eq_thm_prop
    6.15    )
    6.16    val get = Data.get o Context.Proof
    6.17  
     7.1 --- a/src/HOL/Statespace/state_fun.ML	Sun Nov 08 16:28:18 2009 +0100
     7.2 +++ b/src/HOL/Statespace/state_fun.ML	Sun Nov 08 16:30:41 2009 +0100
     7.3 @@ -93,20 +93,16 @@
     7.4  
     7.5  val ex_lookup_ss = HOL_ss addsimps @{thms StateFun.ex_id};
     7.6  
     7.7 -structure StateFunArgs =
     7.8 -struct
     7.9 -  type T = (simpset * simpset * bool); 
    7.10 +
    7.11 +structure StateFunData = Generic_Data
    7.12 +(
    7.13 +  type T = simpset * simpset * bool;
    7.14             (* lookup simpset, ex_lookup simpset, are simprocs installed *)
    7.15    val empty = (empty_ss, empty_ss, false);
    7.16    val extend = I;
    7.17 -  fun merge pp ((ss1,ex_ss1,b1),(ss2,ex_ss2,b2)) = 
    7.18 -               (merge_ss (ss1,ss2)
    7.19 -               ,merge_ss (ex_ss1,ex_ss2)
    7.20 -               ,b1 orelse b2);
    7.21 -end;
    7.22 -
    7.23 -
    7.24 -structure StateFunData = GenericDataFun(StateFunArgs);
    7.25 +  fun merge ((ss1, ex_ss1, b1), (ss2, ex_ss2, b2)) =
    7.26 +    (merge_ss (ss1, ss2), merge_ss (ex_ss1, ex_ss2), b1 orelse b2);
    7.27 +);
    7.28  
    7.29  val init_state_fun_data =
    7.30    Context.theory_map (StateFunData.put (lookup_ss,ex_lookup_ss,false));
     8.1 --- a/src/HOL/Statespace/state_space.ML	Sun Nov 08 16:28:18 2009 +0100
     8.2 +++ b/src/HOL/Statespace/state_space.ML	Sun Nov 08 16:30:41 2009 +0100
     8.3 @@ -106,19 +106,18 @@
     8.4    silent: bool
     8.5   };
     8.6  
     8.7 -structure NameSpaceArgs =
     8.8 -struct
     8.9 +structure NameSpaceData = Generic_Data
    8.10 +(
    8.11    type T = namespace_info;
    8.12    val empty = {declinfo = Termtab.empty, distinctthm = Symtab.empty, silent = false};
    8.13    val extend = I;
    8.14 -  fun merge pp ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
    8.15 -                {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) =
    8.16 -                {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
    8.17 -                 distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
    8.18 -                 silent = silent1 andalso silent2}
    8.19 -end;
    8.20 -
    8.21 -structure NameSpaceData = GenericDataFun(NameSpaceArgs);
    8.22 +  fun merge
    8.23 +    ({declinfo=declinfo1, distinctthm=distinctthm1, silent=silent1},
    8.24 +      {declinfo=declinfo2, distinctthm=distinctthm2, silent=silent2}) : T =
    8.25 +    {declinfo = Termtab.merge (K true) (declinfo1, declinfo2),
    8.26 +     distinctthm = Symtab.merge (K true) (distinctthm1, distinctthm2),
    8.27 +     silent = silent1 andalso silent2}
    8.28 +);
    8.29  
    8.30  fun make_namespace_data declinfo distinctthm silent =
    8.31       {declinfo=declinfo,distinctthm=distinctthm,silent=silent};
    8.32 @@ -172,17 +171,13 @@
    8.33    types: typ list (* range types of state space *)
    8.34   };
    8.35  
    8.36 -structure StateSpaceArgs =
    8.37 -struct
    8.38 -  val name = "HOL/StateSpace";
    8.39 +structure StateSpaceData = Generic_Data
    8.40 +(
    8.41    type T = statespace_info Symtab.table;
    8.42    val empty = Symtab.empty;
    8.43    val extend = I;
    8.44 -
    8.45 -  fun merge pp (nt1,nt2) = Symtab.merge (K true) (nt1, nt2);
    8.46 -end;
    8.47 -
    8.48 -structure StateSpaceData = GenericDataFun(StateSpaceArgs);
    8.49 +  fun merge data : T = Symtab.merge (K true) data;
    8.50 +);
    8.51  
    8.52  fun add_statespace name args parents components types ctxt =
    8.53       StateSpaceData.put
     9.1 --- a/src/HOL/Tools/Function/context_tree.ML	Sun Nov 08 16:28:18 2009 +0100
     9.2 +++ b/src/HOL/Tools/Function/context_tree.ML	Sun Nov 08 16:30:41 2009 +0100
     9.3 @@ -44,12 +44,12 @@
     9.4  open Function_Common
     9.5  open Function_Lib
     9.6  
     9.7 -structure FunctionCongs = GenericDataFun
     9.8 +structure FunctionCongs = Generic_Data
     9.9  (
    9.10    type T = thm list
    9.11    val empty = []
    9.12    val extend = I
    9.13 -  fun merge _ = Thm.merge_thms
    9.14 +  val merge = Thm.merge_thms
    9.15  );
    9.16  
    9.17  val get_function_congs = FunctionCongs.get o Context.Proof
    10.1 --- a/src/HOL/Tools/Function/function_common.ML	Sun Nov 08 16:28:18 2009 +0100
    10.2 +++ b/src/HOL/Tools/Function/function_common.ML	Sun Nov 08 16:30:41 2009 +0100
    10.3 @@ -27,12 +27,12 @@
    10.4  
    10.5  (* Termination rules *)
    10.6  
    10.7 -structure TerminationRule = GenericDataFun
    10.8 +structure TerminationRule = Generic_Data
    10.9  (
   10.10    type T = thm list
   10.11    val empty = []
   10.12    val extend = I
   10.13 -  fun merge _ = Thm.merge_thms
   10.14 +  val merge = Thm.merge_thms
   10.15  );
   10.16  
   10.17  val get_termination_rules = TerminationRule.get
   10.18 @@ -90,13 +90,12 @@
   10.19                        defname = name defname }
   10.20      end
   10.21  
   10.22 -structure FunctionData = GenericDataFun
   10.23 +structure FunctionData = Generic_Data
   10.24  (
   10.25    type T = (term * function_context_data) Item_Net.T;
   10.26    val empty : T = Item_Net.init (op aconv o pairself fst) (single o fst);
   10.27 -  val copy = I;
   10.28    val extend = I;
   10.29 -  fun merge _ (tab1, tab2) = Item_Net.merge (tab1, tab2)
   10.30 +  fun merge tabs : T = Item_Net.merge tabs;
   10.31  );
   10.32  
   10.33  val get_function = FunctionData.get o Context.Proof;
   10.34 @@ -152,12 +151,12 @@
   10.35  
   10.36  (* Default Termination Prover *)
   10.37  
   10.38 -structure TerminationProver = GenericDataFun
   10.39 +structure TerminationProver = Generic_Data
   10.40  (
   10.41    type T = Proof.context -> Proof.method
   10.42    val empty = (fn _ => error "Termination prover not configured")
   10.43    val extend = I
   10.44 -  fun merge _ (a,b) = b (* FIXME *)
   10.45 +  fun merge (a, b) = b  (* FIXME ? *)
   10.46  );
   10.47  
   10.48  val set_termination_prover = TerminationProver.put
   10.49 @@ -310,12 +309,12 @@
   10.50        (ts, curry op ~~ bnds o Library.unflat tss, sort, cnames)
   10.51      end
   10.52  
   10.53 -structure Preprocessor = GenericDataFun
   10.54 +structure Preprocessor = Generic_Data
   10.55  (
   10.56    type T = preproc
   10.57    val empty : T = empty_preproc check_defs
   10.58    val extend = I
   10.59 -  fun merge _ (a, _) = a
   10.60 +  fun merge (a, _) = a
   10.61  );
   10.62  
   10.63  val get_preproc = Preprocessor.get o Context.Proof
    11.1 --- a/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sun Nov 08 16:28:18 2009 +0100
    11.2 +++ b/src/HOL/Tools/Groebner_Basis/normalizer_data.ML	Sun Nov 08 16:30:41 2009 +0100
    11.3 @@ -40,12 +40,12 @@
    11.4  val eq_key = Thm.eq_thm;
    11.5  fun eq_data arg = eq_fst eq_key arg;
    11.6  
    11.7 -structure Data = GenericDataFun
    11.8 +structure Data = Generic_Data
    11.9  (
   11.10    type T = simpset * (thm * entry) list;
   11.11    val empty = (HOL_basic_ss, []);
   11.12    val extend = I;
   11.13 -  fun merge _ ((ss, e), (ss', e')) =
   11.14 +  fun merge ((ss, e), (ss', e')) : T =
   11.15      (merge_ss (ss, ss'), AList.merge eq_key (K true) (e, e'));
   11.16  );
   11.17  
    12.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 16:28:18 2009 +0100
    12.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML	Sun Nov 08 16:30:41 2009 +0100
    12.3 @@ -2450,7 +2450,7 @@
    12.4    (*FIXME name discrepancy in attribs and ML code*)
    12.5    (*FIXME intros should be better named intro*)
    12.6  
    12.7 -(* TODO: make TheoryDataFun to GenericDataFun & remove duplication of local theory and theory *)
    12.8 +(* TODO: make TheoryDataFun to Generic_Data & remove duplication of local theory and theory *)
    12.9  fun generic_code_pred prep_const options raw_const lthy =
   12.10    let
   12.11      val thy = ProofContext.theory_of lthy
    13.1 --- a/src/HOL/Tools/Qelim/cooper_data.ML	Sun Nov 08 16:28:18 2009 +0100
    13.2 +++ b/src/HOL/Tools/Qelim/cooper_data.ML	Sun Nov 08 16:30:41 2009 +0100
    13.3 @@ -44,12 +44,12 @@
    13.4     @{term "0::int"}, @{term "1::int"}, @{term "0::nat"}, @{term "1::nat"},
    13.5     @{term "True"}, @{term "False"}];
    13.6  
    13.7 -structure Data = GenericDataFun
    13.8 +structure Data = Generic_Data
    13.9  (
   13.10 -  type T = simpset * (term list);
   13.11 +  type T = simpset * term list;
   13.12    val empty = (start_ss, allowed_consts);
   13.13    val extend  = I;
   13.14 -  fun merge _ ((ss1, ts1), (ss2, ts2)) =
   13.15 +  fun merge ((ss1, ts1), (ss2, ts2)) =
   13.16      (merge_ss (ss1, ss2), Library.merge (op aconv) (ts1, ts2));
   13.17  );
   13.18  
    14.1 --- a/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sun Nov 08 16:28:18 2009 +0100
    14.2 +++ b/src/HOL/Tools/Qelim/ferrante_rackoff_data.ML	Sun Nov 08 16:30:41 2009 +0100
    14.3 @@ -38,12 +38,12 @@
    14.4  val eq_key = Thm.eq_thm;
    14.5  fun eq_data arg = eq_fst eq_key arg;
    14.6  
    14.7 -structure Data = GenericDataFun
    14.8 +structure Data = Generic_Data
    14.9  (
   14.10    type T = (thm * entry) list;
   14.11    val empty = [];
   14.12    val extend = I;
   14.13 -  fun merge _ = AList.merge eq_key (K true);
   14.14 +  fun merge data : T = AList.merge eq_key (K true) data;
   14.15  );
   14.16  
   14.17  val get = Data.get o Context.Proof;
    15.1 --- a/src/HOL/Tools/Qelim/langford_data.ML	Sun Nov 08 16:28:18 2009 +0100
    15.2 +++ b/src/HOL/Tools/Qelim/langford_data.ML	Sun Nov 08 16:30:41 2009 +0100
    15.3 @@ -17,12 +17,13 @@
    15.4  val eq_key = Thm.eq_thm;
    15.5  fun eq_data arg = eq_fst eq_key arg;
    15.6  
    15.7 -structure Data = GenericDataFun
    15.8 -( type T = simpset * (thm * entry) list;
    15.9 +structure Data = Generic_Data
   15.10 +(
   15.11 +  type T = simpset * (thm * entry) list;
   15.12    val empty = (HOL_basic_ss, []);
   15.13    val extend = I;
   15.14 -  fun merge _ ((ss1,es1), (ss2,es2)) = 
   15.15 -       (merge_ss (ss1,ss2), AList.merge eq_key (K true) (es1,es2));;
   15.16 +  fun merge ((ss1, es1), (ss2, es2)) : T =
   15.17 +    (merge_ss (ss1, ss2), AList.merge eq_key (K true) (es1, es2));
   15.18  );
   15.19  
   15.20  val get = Data.get o Context.Proof;
    16.1 --- a/src/HOL/Tools/inductive.ML	Sun Nov 08 16:28:18 2009 +0100
    16.2 +++ b/src/HOL/Tools/inductive.ML	Sun Nov 08 16:30:41 2009 +0100
    16.3 @@ -136,12 +136,12 @@
    16.4  type inductive_info =
    16.5    {names: string list, coind: bool} * inductive_result;
    16.6  
    16.7 -structure InductiveData = GenericDataFun
    16.8 +structure InductiveData = Generic_Data
    16.9  (
   16.10    type T = inductive_info Symtab.table * thm list;
   16.11    val empty = (Symtab.empty, []);
   16.12    val extend = I;
   16.13 -  fun merge _ ((tab1, monos1), (tab2, monos2)) =
   16.14 +  fun merge ((tab1, monos1), (tab2, monos2)) : T =
   16.15      (Symtab.merge (K true) (tab1, tab2), Thm.merge_thms (monos1, monos2));
   16.16  );
   16.17  
    17.1 --- a/src/HOL/Tools/inductive_set.ML	Sun Nov 08 16:28:18 2009 +0100
    17.2 +++ b/src/HOL/Tools/inductive_set.ML	Sun Nov 08 16:30:41 2009 +0100
    17.3 @@ -152,7 +152,7 @@
    17.4  (* where s and p are parameters                            *)
    17.5  (***********************************************************)
    17.6  
    17.7 -structure PredSetConvData = GenericDataFun
    17.8 +structure PredSetConvData = Generic_Data
    17.9  (
   17.10    type T =
   17.11      {(* rules for converting predicates to sets *)
   17.12 @@ -166,7 +166,7 @@
   17.13    val empty = {to_set_simps = [], to_pred_simps = [],
   17.14      set_arities = Symtab.empty, pred_arities = Symtab.empty};
   17.15    val extend = I;
   17.16 -  fun merge _
   17.17 +  fun merge
   17.18      ({to_set_simps = to_set_simps1, to_pred_simps = to_pred_simps1,
   17.19        set_arities = set_arities1, pred_arities = pred_arities1},
   17.20       {to_set_simps = to_set_simps2, to_pred_simps = to_pred_simps2,
    18.1 --- a/src/HOL/Tools/lin_arith.ML	Sun Nov 08 16:28:18 2009 +0100
    18.2 +++ b/src/HOL/Tools/lin_arith.ML	Sun Nov 08 16:30:41 2009 +0100
    18.3 @@ -72,14 +72,14 @@
    18.4  
    18.5  (* arith context data *)
    18.6  
    18.7 -structure Lin_Arith_Data = GenericDataFun
    18.8 +structure Lin_Arith_Data = Generic_Data
    18.9  (
   18.10    type T = {splits: thm list,
   18.11              inj_consts: (string * typ) list,
   18.12              discrete: string list};
   18.13    val empty = {splits = [], inj_consts = [], discrete = []};
   18.14    val extend = I;
   18.15 -  fun merge _
   18.16 +  fun merge
   18.17     ({splits= splits1, inj_consts= inj_consts1, discrete= discrete1},
   18.18      {splits= splits2, inj_consts= inj_consts2, discrete= discrete2}) : T =
   18.19     {splits = Library.merge Thm.eq_thm_prop (splits1, splits2),
    19.1 --- a/src/HOL/Tools/recdef.ML	Sun Nov 08 16:28:18 2009 +0100
    19.2 +++ b/src/HOL/Tools/recdef.ML	Sun Nov 08 16:30:41 2009 +0100
    19.3 @@ -115,7 +115,7 @@
    19.4  
    19.5  (* proof data *)
    19.6  
    19.7 -structure LocalRecdefData = ProofDataFun
    19.8 +structure LocalRecdefData = Proof_Data
    19.9  (
   19.10    type T = hints;
   19.11    val init = get_global_hints;
    20.1 --- a/src/HOL/Tools/res_blacklist.ML	Sun Nov 08 16:28:18 2009 +0100
    20.2 +++ b/src/HOL/Tools/res_blacklist.ML	Sun Nov 08 16:30:41 2009 +0100
    20.3 @@ -19,12 +19,12 @@
    20.4  structure Res_Blacklist: RES_BLACKLIST =
    20.5  struct
    20.6  
    20.7 -structure Data = GenericDataFun
    20.8 +structure Data = Generic_Data
    20.9  (
   20.10    type T = thm Termtab.table;
   20.11    val empty = Termtab.empty;
   20.12    val extend = I;
   20.13 -  fun merge _ tabs = Termtab.merge (K true) tabs;
   20.14 +  fun merge tabs = Termtab.merge (K true) tabs;
   20.15  );
   20.16  
   20.17  fun blacklisted ctxt th =
    21.1 --- a/src/HOL/Tools/transfer.ML	Sun Nov 08 16:28:18 2009 +0100
    21.2 +++ b/src/HOL/Tools/transfer.ML	Sun Nov 08 16:30:41 2009 +0100
    21.3 @@ -25,12 +25,12 @@
    21.4  
    21.5  type data = simpset * (thm * entry) list;
    21.6  
    21.7 -structure Data = GenericDataFun
    21.8 +structure Data = Generic_Data
    21.9  (
   21.10    type T = data;
   21.11    val empty = (HOL_ss, []);
   21.12    val extend  = I;
   21.13 -  fun merge _ ((ss1, e1), (ss2, e2)) =
   21.14 +  fun merge ((ss1, e1), (ss2, e2)) : T =
   21.15      (merge_ss (ss1, ss2), AList.join Thm.eq_thm (K merge_entry) (e1, e2));
   21.16  );
   21.17  
    22.1 --- a/src/HOLCF/Tools/fixrec.ML	Sun Nov 08 16:28:18 2009 +0100
    22.2 +++ b/src/HOLCF/Tools/fixrec.ML	Sun Nov 08 16:30:41 2009 +0100
    22.3 @@ -160,12 +160,12 @@
    22.4  (************* fixed-point definitions and unfolding theorems ************)
    22.5  (*************************************************************************)
    22.6  
    22.7 -structure FixrecUnfoldData = GenericDataFun (
    22.8 +structure FixrecUnfoldData = Generic_Data
    22.9 +(
   22.10    type T = thm Symtab.table;
   22.11    val empty = Symtab.empty;
   22.12 -  val copy = I;
   22.13    val extend = I;
   22.14 -  fun merge _ = Symtab.merge (K true);
   22.15 +  fun merge data : T = Symtab.merge (K true) data;
   22.16  );
   22.17  
   22.18  local
   22.19 @@ -363,16 +363,16 @@
   22.20  (********************** Proving associated theorems **********************)
   22.21  (*************************************************************************)
   22.22  
   22.23 -structure FixrecSimpData = GenericDataFun (
   22.24 +structure FixrecSimpData = Generic_Data
   22.25 +(
   22.26    type T = simpset;
   22.27    val empty =
   22.28      HOL_basic_ss
   22.29        addsimps simp_thms
   22.30        addsimps [@{thm beta_cfun}]
   22.31        addsimprocs [@{simproc cont_proc}];
   22.32 -  val copy = I;
   22.33    val extend = I;
   22.34 -  fun merge _ = merge_ss;
   22.35 +  val merge = merge_ss;
   22.36  );
   22.37  
   22.38  fun fixrec_simp_tac ctxt =
    23.1 --- a/src/Provers/Arith/fast_lin_arith.ML	Sun Nov 08 16:28:18 2009 +0100
    23.2 +++ b/src/Provers/Arith/fast_lin_arith.ML	Sun Nov 08 16:30:41 2009 +0100
    23.3 @@ -109,7 +109,7 @@
    23.4  
    23.5  fun no_number_of _ _ _ = raise CTERM ("number_of", [])
    23.6  
    23.7 -structure Data = GenericDataFun
    23.8 +structure Data = Generic_Data
    23.9  (
   23.10    type T =
   23.11     {add_mono_thms: thm list,
   23.12 @@ -124,7 +124,7 @@
   23.13                 lessD = [], neqE = [], simpset = Simplifier.empty_ss,
   23.14                 number_of = (serial (), no_number_of) } : T;
   23.15    val extend = I;
   23.16 -  fun merge _
   23.17 +  fun merge
   23.18      ({add_mono_thms= add_mono_thms1, mult_mono_thms= mult_mono_thms1, inj_thms= inj_thms1,
   23.19        lessD = lessD1, neqE=neqE1, simpset = simpset1,
   23.20        number_of = (number_of1 as (s1, _))},
   23.21 @@ -137,6 +137,7 @@
   23.22       lessD = Thm.merge_thms (lessD1, lessD2),
   23.23       neqE = Thm.merge_thms (neqE1, neqE2),
   23.24       simpset = Simplifier.merge_ss (simpset1, simpset2),
   23.25 +     (* FIXME depends on accidental load order !?! *)
   23.26       number_of = if s1 > s2 then number_of1 else number_of2};
   23.27  );
   23.28  
    24.1 --- a/src/Provers/classical.ML	Sun Nov 08 16:28:18 2009 +0100
    24.2 +++ b/src/Provers/classical.ML	Sun Nov 08 16:30:41 2009 +0100
    24.3 @@ -868,7 +868,7 @@
    24.4  
    24.5  (* local clasets *)
    24.6  
    24.7 -structure LocalClaset = ProofDataFun
    24.8 +structure LocalClaset = Proof_Data
    24.9  (
   24.10    type T = claset;
   24.11    val init = get_global_claset;
    25.1 --- a/src/Pure/Isar/calculation.ML	Sun Nov 08 16:28:18 2009 +0100
    25.2 +++ b/src/Pure/Isar/calculation.ML	Sun Nov 08 16:30:41 2009 +0100
    25.3 @@ -27,13 +27,12 @@
    25.4  
    25.5  (** calculation data **)
    25.6  
    25.7 -structure CalculationData = GenericDataFun
    25.8 +structure CalculationData = Generic_Data
    25.9  (
   25.10    type T = (thm Item_Net.T * thm list) * (thm list * int) option;
   25.11    val empty = ((Thm.elim_rules, []), NONE);
   25.12    val extend = I;
   25.13 -
   25.14 -  fun merge _ (((trans1, sym1), _), ((trans2, sym2), _)) =
   25.15 +  fun merge (((trans1, sym1), _), ((trans2, sym2), _)) =
   25.16      ((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
   25.17  );
   25.18  
    26.1 --- a/src/Pure/Isar/class_target.ML	Sun Nov 08 16:28:18 2009 +0100
    26.2 +++ b/src/Pure/Isar/class_target.ML	Sun Nov 08 16:30:41 2009 +0100
    26.3 @@ -398,7 +398,7 @@
    26.4      (*(instantiation parameter, type constructor), (local instantiation parameter, typ)*)
    26.5  }
    26.6  
    26.7 -structure Instantiation = ProofDataFun
    26.8 +structure Instantiation = Proof_Data
    26.9  (
   26.10    type T = instantiation
   26.11    fun init _ = Instantiation { arities = ([], [], []), params = [] };
    27.1 --- a/src/Pure/Isar/code.ML	Sun Nov 08 16:28:18 2009 +0100
    27.2 +++ b/src/Pure/Isar/code.ML	Sun Nov 08 16:30:41 2009 +0100
    27.3 @@ -794,12 +794,12 @@
    27.4  structure Predicate_Compile_Preproc_Const_Defs : PREDICATE_COMPILE_PREPROC_CONST_DEFS =
    27.5  struct
    27.6  
    27.7 -structure Data = GenericDataFun
    27.8 +structure Data = Generic_Data
    27.9  (
   27.10    type T = thm list;
   27.11    val empty = [];
   27.12    val extend = I;
   27.13 -  fun merge _ = Thm.merge_thms;
   27.14 +  val merge = Thm.merge_thms;
   27.15  );
   27.16  
   27.17  val get = Data.get o Context.Proof;
    28.1 --- a/src/Pure/Isar/context_rules.ML	Sun Nov 08 16:28:18 2009 +0100
    28.2 +++ b/src/Pure/Isar/context_rules.ML	Sun Nov 08 16:30:41 2009 +0100
    28.3 @@ -89,13 +89,13 @@
    28.4      else make_rules next (filter_out eq_th rules) (map (del false o del true) netpairs) wrappers
    28.5    end;
    28.6  
    28.7 -structure Rules = GenericDataFun
    28.8 +structure Rules = Generic_Data
    28.9  (
   28.10    type T = rules;
   28.11    val empty = make_rules ~1 [] empty_netpairs ([], []);
   28.12    val extend = I;
   28.13 -
   28.14 -  fun merge _ (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
   28.15 +  fun merge
   28.16 +    (Rules {rules = rules1, wrappers = (ws1, ws1'), ...},
   28.17        Rules {rules = rules2, wrappers = (ws2, ws2'), ...}) =
   28.18      let
   28.19        val wrappers =
    29.1 --- a/src/Pure/Isar/local_defs.ML	Sun Nov 08 16:28:18 2009 +0100
    29.2 +++ b/src/Pure/Isar/local_defs.ML	Sun Nov 08 16:30:41 2009 +0100
    29.3 @@ -186,12 +186,12 @@
    29.4  
    29.5  (* transformation rules *)
    29.6  
    29.7 -structure Rules = GenericDataFun
    29.8 +structure Rules = Generic_Data
    29.9  (
   29.10    type T = thm list;
   29.11 -  val empty = []
   29.12 +  val empty = [];
   29.13    val extend = I;
   29.14 -  fun merge _ = Thm.merge_thms;
   29.15 +  val merge = Thm.merge_thms;
   29.16  );
   29.17  
   29.18  fun print_rules ctxt =
    30.1 --- a/src/Pure/Isar/local_theory.ML	Sun Nov 08 16:28:18 2009 +0100
    30.2 +++ b/src/Pure/Isar/local_theory.ML	Sun Nov 08 16:30:41 2009 +0100
    30.3 @@ -85,7 +85,7 @@
    30.4  
    30.5  (* context data *)
    30.6  
    30.7 -structure Data = ProofDataFun
    30.8 +structure Data = Proof_Data
    30.9  (
   30.10    type T = lthy option;
   30.11    fun init _ = NONE;
    31.1 --- a/src/Pure/Isar/locale.ML	Sun Nov 08 16:28:18 2009 +0100
    31.2 +++ b/src/Pure/Isar/locale.ML	Sun Nov 08 16:30:41 2009 +0100
    31.3 @@ -188,12 +188,12 @@
    31.4  
    31.5  datatype 'a delayed = Ready of 'a | ToDo of 'a delayed * 'a delayed;
    31.6  
    31.7 -structure Identifiers = GenericDataFun
    31.8 +structure Identifiers = Generic_Data
    31.9  (
   31.10    type T = (string * term list) list delayed;
   31.11    val empty = Ready [];
   31.12    val extend = I;
   31.13 -  fun merge _ = ToDo;
   31.14 +  val merge = ToDo;
   31.15  );
   31.16  
   31.17  fun finish thy (ToDo (i1, i2)) = merge (ident_eq thy) (finish thy i1, finish thy i2)
   31.18 @@ -569,12 +569,12 @@
   31.19  
   31.20  (* Storage for witnesses, intro and unfold rules *)
   31.21  
   31.22 -structure Thms = GenericDataFun
   31.23 +structure Thms = Generic_Data
   31.24  (
   31.25    type T = thm list * thm list * thm list;
   31.26    val empty = ([], [], []);
   31.27    val extend = I;
   31.28 -  fun merge _ ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   31.29 +  fun merge ((witnesses1, intros1, unfolds1), (witnesses2, intros2, unfolds2)) =
   31.30     (Thm.merge_thms (witnesses1, witnesses2),
   31.31      Thm.merge_thms (intros1, intros2),
   31.32      Thm.merge_thms (unfolds1, unfolds2));
    32.1 --- a/src/Pure/Isar/method.ML	Sun Nov 08 16:28:18 2009 +0100
    32.2 +++ b/src/Pure/Isar/method.ML	Sun Nov 08 16:30:41 2009 +0100
    32.3 @@ -270,7 +270,7 @@
    32.4  
    32.5  (* ML tactics *)
    32.6  
    32.7 -structure TacticData = ProofDataFun
    32.8 +structure TacticData = Proof_Data
    32.9  (
   32.10    type T = thm list -> tactic;
   32.11    fun init _ = undefined;
    33.1 --- a/src/Pure/Isar/overloading.ML	Sun Nov 08 16:28:18 2009 +0100
    33.2 +++ b/src/Pure/Isar/overloading.ML	Sun Nov 08 16:30:41 2009 +0100
    33.3 @@ -30,7 +30,8 @@
    33.4    ((((string * typ -> (typ * typ) option) * (string * typ -> (typ * term) option)) * bool) *
    33.5      (term * term) list)) * bool);
    33.6  
    33.7 -structure ImprovableSyntax = ProofDataFun(
    33.8 +structure ImprovableSyntax = Proof_Data
    33.9 +(
   33.10    type T = {
   33.11      primary_constraints: (string * typ) list,
   33.12      secondary_constraints: (string * typ) list,
   33.13 @@ -119,7 +120,7 @@
   33.14  
   33.15  (* bookkeeping *)
   33.16  
   33.17 -structure OverloadingData = ProofDataFun
   33.18 +structure OverloadingData = Proof_Data
   33.19  (
   33.20    type T = ((string * typ) * (string * bool)) list;
   33.21    fun init _ = [];
    34.1 --- a/src/Pure/Isar/proof_context.ML	Sun Nov 08 16:28:18 2009 +0100
    34.2 +++ b/src/Pure/Isar/proof_context.ML	Sun Nov 08 16:30:41 2009 +0100
    34.3 @@ -177,7 +177,7 @@
    34.4  
    34.5  val local_naming = Name_Space.default_naming |> Name_Space.add_path "local";
    34.6  
    34.7 -structure ContextData = ProofDataFun
    34.8 +structure ContextData = Proof_Data
    34.9  (
   34.10    type T = ctxt;
   34.11    fun init thy =
   34.12 @@ -515,7 +515,7 @@
   34.13  
   34.14  local
   34.15  
   34.16 -structure Allow_Dummies = ProofDataFun(type T = bool fun init _ = false);
   34.17 +structure Allow_Dummies = Proof_Data(type T = bool fun init _ = false);
   34.18  
   34.19  fun check_dummies ctxt t =
   34.20    if Allow_Dummies.get ctxt then t
    35.1 --- a/src/Pure/Isar/spec_rules.ML	Sun Nov 08 16:28:18 2009 +0100
    35.2 +++ b/src/Pure/Isar/spec_rules.ML	Sun Nov 08 16:30:41 2009 +0100
    35.3 @@ -24,7 +24,7 @@
    35.4  datatype rough_classification = Unknown | Equational | Inductive | Co_Inductive;
    35.5  type spec = rough_classification * (term list * thm list);
    35.6  
    35.7 -structure Rules = GenericDataFun
    35.8 +structure Rules = Generic_Data
    35.9  (
   35.10    type T = spec Item_Net.T;
   35.11    val empty : T =
   35.12 @@ -35,7 +35,7 @@
   35.13          eq_list Thm.eq_thm_prop (ths1, ths2))
   35.14        (#1 o #2);
   35.15    val extend = I;
   35.16 -  fun merge _ = Item_Net.merge;
   35.17 +  fun merge data = Item_Net.merge data;
   35.18  );
   35.19  
   35.20  val get = Item_Net.content o Rules.get o Context.Proof;
    36.1 --- a/src/Pure/Isar/specification.ML	Sun Nov 08 16:28:18 2009 +0100
    36.2 +++ b/src/Pure/Isar/specification.ML	Sun Nov 08 16:30:41 2009 +0100
    36.3 @@ -333,12 +333,12 @@
    36.4                  [((Binding.name Obtain.thatN, []), [(ths, [])])] #> #2 #> pair ths);
    36.5        in ((prems, stmt, SOME facts), goal_ctxt) end);
    36.6  
    36.7 -structure TheoremHook = GenericDataFun
    36.8 +structure TheoremHook = Generic_Data
    36.9  (
   36.10    type T = ((bool -> Proof.state -> Proof.state) * stamp) list;
   36.11    val empty = [];
   36.12    val extend = I;
   36.13 -  fun merge _ hooks : T = Library.merge (eq_snd op =) hooks;
   36.14 +  fun merge hooks : T = Library.merge (eq_snd op =) hooks;
   36.15  );
   36.16  
   36.17  fun gen_theorem prep_att prep_stmt
    37.1 --- a/src/Pure/Isar/theory_target.ML	Sun Nov 08 16:28:18 2009 +0100
    37.2 +++ b/src/Pure/Isar/theory_target.ML	Sun Nov 08 16:30:41 2009 +0100
    37.3 @@ -34,7 +34,7 @@
    37.4  
    37.5  val global_target = make_target "" false false ([], [], []) [];
    37.6  
    37.7 -structure Data = ProofDataFun
    37.8 +structure Data = Proof_Data
    37.9  (
   37.10    type T = target;
   37.11    fun init _ = global_target;
    38.1 --- a/src/Pure/Isar/toplevel.ML	Sun Nov 08 16:28:18 2009 +0100
    38.2 +++ b/src/Pure/Isar/toplevel.ML	Sun Nov 08 16:30:41 2009 +0100
    38.3 @@ -631,7 +631,7 @@
    38.4  
    38.5  (* excursion of units, consisting of commands with proof *)
    38.6  
    38.7 -structure States = ProofDataFun
    38.8 +structure States = Proof_Data
    38.9  (
   38.10    type T = state list future option;
   38.11    fun init _ = NONE;
    39.1 --- a/src/Pure/ML/ml_antiquote.ML	Sun Nov 08 16:28:18 2009 +0100
    39.2 +++ b/src/Pure/ML/ml_antiquote.ML	Sun Nov 08 16:30:41 2009 +0100
    39.3 @@ -20,7 +20,7 @@
    39.4  
    39.5  (* ML names *)
    39.6  
    39.7 -structure NamesData = ProofDataFun
    39.8 +structure NamesData = Proof_Data
    39.9  (
   39.10    type T = Name.context;
   39.11    fun init _ = ML_Syntax.reserved;
    40.1 --- a/src/Pure/ML/ml_env.ML	Sun Nov 08 16:28:18 2009 +0100
    40.2 +++ b/src/Pure/ML/ml_env.ML	Sun Nov 08 16:30:41 2009 +0100
    40.3 @@ -16,7 +16,7 @@
    40.4  
    40.5  (* context data *)
    40.6  
    40.7 -structure Env = GenericDataFun
    40.8 +structure Env = Generic_Data
    40.9  (
   40.10    type T =
   40.11      ML_Name_Space.valueVal Symtab.table *
   40.12 @@ -27,7 +27,7 @@
   40.13      ML_Name_Space.functorVal Symtab.table;
   40.14    val empty = (Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty, Symtab.empty);
   40.15    val extend = I;
   40.16 -  fun merge _
   40.17 +  fun merge
   40.18     ((val1, type1, fixity1, structure1, signature1, functor1),
   40.19      (val2, type2, fixity2, structure2, signature2, functor2)) : T =
   40.20      (Symtab.merge (K true) (val1, val2),
    41.1 --- a/src/Pure/ML/ml_thms.ML	Sun Nov 08 16:28:18 2009 +0100
    41.2 +++ b/src/Pure/ML/ml_thms.ML	Sun Nov 08 16:30:41 2009 +0100
    41.3 @@ -15,7 +15,7 @@
    41.4  
    41.5  (* auxiliary facts table *)
    41.6  
    41.7 -structure AuxFacts = ProofDataFun
    41.8 +structure AuxFacts = Proof_Data
    41.9  (
   41.10    type T = thm list Inttab.table;
   41.11    fun init _ = Inttab.empty;
    42.1 --- a/src/Pure/Syntax/syntax.ML	Sun Nov 08 16:28:18 2009 +0100
    42.2 +++ b/src/Pure/Syntax/syntax.ML	Sun Nov 08 16:30:41 2009 +0100
    42.3 @@ -741,14 +741,14 @@
    42.4  type key = int * bool;
    42.5  type 'a check = 'a list -> Proof.context -> ('a list * Proof.context) option;
    42.6  
    42.7 -structure Checks = GenericDataFun
    42.8 +structure Checks = Generic_Data
    42.9  (
   42.10    type T =
   42.11      ((key * ((string * typ check) * stamp) list) list *
   42.12       (key * ((string * term check) * stamp) list) list);
   42.13    val empty = ([], []);
   42.14    val extend = I;
   42.15 -  fun merge _ ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
   42.16 +  fun merge ((typ_checks1, term_checks1), (typ_checks2, term_checks2)) : T =
   42.17      (AList.join (op =) (K (Library.merge (eq_snd (op =)))) (typ_checks1, typ_checks2),
   42.18       AList.join (op =) (K (Library.merge (eq_snd (op =)))) (term_checks1, term_checks2));
   42.19  );
   42.20 @@ -877,7 +877,7 @@
   42.21  
   42.22  (* global pretty printing *)
   42.23  
   42.24 -structure PrettyGlobal = ProofDataFun(type T = bool fun init _ = false);
   42.25 +structure PrettyGlobal = Proof_Data(type T = bool fun init _ = false);
   42.26  val is_pretty_global = PrettyGlobal.get;
   42.27  val set_pretty_global = PrettyGlobal.put;
   42.28  val init_pretty_global = set_pretty_global true o ProofContext.init;
    43.1 --- a/src/Pure/Tools/named_thms.ML	Sun Nov 08 16:28:18 2009 +0100
    43.2 +++ b/src/Pure/Tools/named_thms.ML	Sun Nov 08 16:30:41 2009 +0100
    43.3 @@ -17,12 +17,12 @@
    43.4  functor Named_Thms(val name: string val description: string): NAMED_THMS =
    43.5  struct
    43.6  
    43.7 -structure Data = GenericDataFun
    43.8 +structure Data = Generic_Data
    43.9  (
   43.10    type T = thm Item_Net.T;
   43.11    val empty = Thm.full_rules;
   43.12    val extend = I;
   43.13 -  fun merge _ = Item_Net.merge;
   43.14 +  val merge = Item_Net.merge;
   43.15  );
   43.16  
   43.17  val content = Item_Net.content o Data.get;
    44.1 --- a/src/Pure/assumption.ML	Sun Nov 08 16:28:18 2009 +0100
    44.2 +++ b/src/Pure/assumption.ML	Sun Nov 08 16:30:41 2009 +0100
    44.3 @@ -60,7 +60,7 @@
    44.4  
    44.5  fun make_data (assms, prems) = Data {assms = assms, prems = prems};
    44.6  
    44.7 -structure Data = ProofDataFun
    44.8 +structure Data = Proof_Data
    44.9  (
   44.10    type T = data;
   44.11    fun init _ = make_data ([], []);
    45.1 --- a/src/Pure/config.ML	Sun Nov 08 16:28:18 2009 +0100
    45.2 +++ b/src/Pure/config.ML	Sun Nov 08 16:30:41 2009 +0100
    45.3 @@ -90,12 +90,12 @@
    45.4  
    45.5  (* context information *)
    45.6  
    45.7 -structure Value = GenericDataFun
    45.8 +structure Value = Generic_Data
    45.9  (
   45.10    type T = value Inttab.table;
   45.11    val empty = Inttab.empty;
   45.12    val extend = I;
   45.13 -  fun merge _ = Inttab.merge (K true);
   45.14 +  fun merge data = Inttab.merge (K true) data;
   45.15  );
   45.16  
   45.17  fun declare global name default =
    46.1 --- a/src/Pure/context_position.ML	Sun Nov 08 16:28:18 2009 +0100
    46.2 +++ b/src/Pure/context_position.ML	Sun Nov 08 16:30:41 2009 +0100
    46.3 @@ -15,7 +15,7 @@
    46.4  structure Context_Position: CONTEXT_POSITION =
    46.5  struct
    46.6  
    46.7 -structure Data = ProofDataFun
    46.8 +structure Data = Proof_Data
    46.9  (
   46.10    type T = bool;
   46.11    fun init _ = true;
    47.1 --- a/src/Pure/simplifier.ML	Sun Nov 08 16:28:18 2009 +0100
    47.2 +++ b/src/Pure/simplifier.ML	Sun Nov 08 16:30:41 2009 +0100
    47.3 @@ -99,12 +99,12 @@
    47.4  
    47.5  (** simpset data **)
    47.6  
    47.7 -structure SimpsetData = GenericDataFun
    47.8 +structure SimpsetData = Generic_Data
    47.9  (
   47.10    type T = simpset;
   47.11    val empty = empty_ss;
   47.12    fun extend ss = MetaSimplifier.inherit_context empty_ss ss;
   47.13 -  fun merge _ = merge_ss;
   47.14 +  val merge = merge_ss;
   47.15  );
   47.16  
   47.17  val get_ss = SimpsetData.get;
   47.18 @@ -145,12 +145,12 @@
   47.19  
   47.20  (* data *)
   47.21  
   47.22 -structure Simprocs = GenericDataFun
   47.23 +structure Simprocs = Generic_Data
   47.24  (
   47.25    type T = simproc Name_Space.table;
   47.26    val empty : T = Name_Space.empty_table "simproc";
   47.27    val extend = I;
   47.28 -  fun merge _ simprocs = Name_Space.merge_tables simprocs;
   47.29 +  fun merge simprocs = Name_Space.merge_tables simprocs;
   47.30  );
   47.31  
   47.32  
    48.1 --- a/src/Pure/type.ML	Sun Nov 08 16:28:18 2009 +0100
    48.2 +++ b/src/Pure/type.ML	Sun Nov 08 16:30:41 2009 +0100
    48.3 @@ -147,7 +147,7 @@
    48.4  val mode_syntax = Mode {normalize = true, logical = false};
    48.5  val mode_abbrev = Mode {normalize = false, logical = false};
    48.6  
    48.7 -structure Mode = ProofDataFun
    48.8 +structure Mode = Proof_Data
    48.9  (
   48.10    type T = mode;
   48.11    fun init _ = mode_default;
    49.1 --- a/src/Pure/variable.ML	Sun Nov 08 16:28:18 2009 +0100
    49.2 +++ b/src/Pure/variable.ML	Sun Nov 08 16:30:41 2009 +0100
    49.3 @@ -86,7 +86,7 @@
    49.4    Data {is_body = is_body, names = names, consts = consts, fixes = fixes, binds = binds,
    49.5      type_occs = type_occs, maxidx = maxidx, sorts = sorts, constraints = constraints};
    49.6  
    49.7 -structure Data = ProofDataFun
    49.8 +structure Data = Proof_Data
    49.9  (
   49.10    type T = data;
   49.11    fun init _ =
    50.1 --- a/src/Tools/Code/code_ml.ML	Sun Nov 08 16:28:18 2009 +0100
    50.2 +++ b/src/Tools/Code/code_ml.ML	Sun Nov 08 16:30:41 2009 +0100
    50.3 @@ -947,7 +947,7 @@
    50.4  
    50.5  local
    50.6  
    50.7 -structure CodeAntiqData = ProofDataFun
    50.8 +structure CodeAntiqData = Proof_Data
    50.9  (
   50.10    type T = (string list * string list) * (bool * (string
   50.11      * (string * ((string * string) list * (string * string) list)) lazy));
    51.1 --- a/src/Tools/induct.ML	Sun Nov 08 16:28:18 2009 +0100
    51.2 +++ b/src/Tools/induct.ML	Sun Nov 08 16:30:41 2009 +0100
    51.3 @@ -130,7 +130,7 @@
    51.4  
    51.5  (* context data *)
    51.6  
    51.7 -structure InductData = GenericDataFun
    51.8 +structure InductData = Generic_Data
    51.9  (
   51.10    type T = (rules * rules) * (rules * rules) * (rules * rules);
   51.11    val empty =
   51.12 @@ -138,7 +138,7 @@
   51.13       (init_rules (right_var_concl o #2), init_rules (Thm.major_prem_of o #2)),
   51.14       (init_rules (left_var_concl o #2), init_rules (Thm.concl_of o #2)));
   51.15    val extend = I;
   51.16 -  fun merge _ (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
   51.17 +  fun merge (((casesT1, casesP1), (inductT1, inductP1), (coinductT1, coinductP1)),
   51.18        ((casesT2, casesP2), (inductT2, inductP2), (coinductT2, coinductP2))) =
   51.19      ((Item_Net.merge (casesT1, casesT2), Item_Net.merge (casesP1, casesP2)),
   51.20        (Item_Net.merge (inductT1, inductT2), Item_Net.merge (inductP1, inductP2)),
    52.1 --- a/src/ZF/Tools/typechk.ML	Sun Nov 08 16:28:18 2009 +0100
    52.2 +++ b/src/ZF/Tools/typechk.ML	Sun Nov 08 16:30:41 2009 +0100
    52.3 @@ -43,15 +43,13 @@
    52.4  
    52.5  (* generic data *)
    52.6  
    52.7 -structure Data = GenericDataFun
    52.8 +structure Data = Generic_Data
    52.9  (
   52.10 -  type T = tcset
   52.11 +  type T = tcset;
   52.12    val empty = TC {rules = [], net = Net.empty};
   52.13    val extend = I;
   52.14 -
   52.15 -  fun merge _ (TC {rules, net}, TC {rules = rules', net = net'}) =
   52.16 -    TC {rules = Thm.merge_thms (rules, rules'),
   52.17 -        net = Net.merge Thm.eq_thm_prop (net, net')};
   52.18 +  fun merge (TC {rules, net}, TC {rules = rules', net = net'}) =
   52.19 +    TC {rules = Thm.merge_thms (rules, rules'), net = Net.merge Thm.eq_thm_prop (net, net')};
   52.20  );
   52.21  
   52.22  val TC_add = Thm.declaration_attribute (Data.map o add_rule);