--- 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 =
--- 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
--- 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. *)
--- 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 =
--- 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
--- 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
--- 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));
--- 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
--- 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
--- 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
--- 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'));
);
--- 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
--- 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));
);
--- 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;
--- 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;
--- 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));
);
--- 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,
--- 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),
--- 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;
--- 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 =
--- 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));
);
--- 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 =
--- 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};
);
--- 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;
--- 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);
);
--- 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 = [] };
--- 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;
--- 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 =
--- 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 =
--- 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;
--- 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));
--- 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;
--- 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 _ = [];
--- 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
--- 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;
--- 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
--- 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;
--- 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;
--- 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;
--- 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),
--- 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;
--- 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;
--- 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;
--- 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 ([], []);
--- 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 =
--- 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;
--- 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;
);
--- 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;
--- 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 _ =
--- 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));
--- 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)),
--- 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);