1.1 --- a/src/HOL/Boogie/Tools/boogie_split.ML Sun Nov 08 18:43:22 2009 +0100
1.2 +++ b/src/HOL/Boogie/Tools/boogie_split.ML Sun Nov 08 18:43:42 2009 +0100
1.3 @@ -18,13 +18,12 @@
1.4
1.5 (* sub-tactics store *)
1.6
1.7 -structure Sub_Tactics = TheoryDataFun
1.8 +structure Sub_Tactics = Theory_Data
1.9 (
1.10 type T = (Proof.context -> int -> tactic) Symtab.table
1.11 val empty = Symtab.empty
1.12 - val copy = I
1.13 val extend = I
1.14 - fun merge _ = Symtab.merge (K true)
1.15 + fun merge data = Symtab.merge (K true) data
1.16 )
1.17
1.18 fun add_sub_tactic tac = Sub_Tactics.map (Symtab.update_new tac)
2.1 --- a/src/HOL/Boogie/Tools/boogie_vcs.ML Sun Nov 08 18:43:22 2009 +0100
2.2 +++ b/src/HOL/Boogie/Tools/boogie_vcs.ML Sun Nov 08 18:43:42 2009 +0100
2.3 @@ -19,14 +19,13 @@
2.4
2.5 fun err_vcs () = error "undischarged Boogie verification conditions found"
2.6
2.7 -structure VCs = TheoryDataFun
2.8 +structure VCs = Theory_Data
2.9 (
2.10 - type T = (Term.term * bool) Symtab.table option
2.11 + type T = (term * bool) Symtab.table option
2.12 val empty = NONE
2.13 - val copy = I
2.14 val extend = I
2.15 - fun merge _ (NONE, NONE) = NONE
2.16 - | merge _ (_, _) = err_vcs ()
2.17 + fun merge (NONE, NONE) = NONE
2.18 + | merge _ = err_vcs ()
2.19 )
2.20
2.21 fun set vcs = VCs.map (fn
3.1 --- a/src/HOL/Import/hol4rews.ML Sun Nov 08 18:43:22 2009 +0100
3.2 +++ b/src/HOL/Import/hol4rews.ML Sun Nov 08 18:43:42 2009 +0100
3.3 @@ -11,25 +11,23 @@
3.4 | Generating of string
3.5 | Replaying of string
3.6
3.7 -structure HOL4DefThy = TheoryDataFun
3.8 +structure HOL4DefThy = Theory_Data
3.9 (
3.10 type T = ImportStatus
3.11 val empty = NoImport
3.12 - val copy = I
3.13 val extend = I
3.14 - fun merge _ (NoImport,NoImport) = NoImport
3.15 - | merge _ _ = (warning "Import status set during merge"; NoImport)
3.16 + fun merge (NoImport, NoImport) = NoImport
3.17 + | merge _ = (warning "Import status set during merge"; NoImport)
3.18 )
3.19
3.20 -structure ImportSegment = TheoryDataFun
3.21 +structure ImportSegment = Theory_Data
3.22 (
3.23 type T = string
3.24 val empty = ""
3.25 - val copy = I
3.26 val extend = I
3.27 - fun merge _ ("",arg) = arg
3.28 - | merge _ (arg,"") = arg
3.29 - | merge _ (s1,s2) =
3.30 + fun merge ("",arg) = arg
3.31 + | merge (arg,"") = arg
3.32 + | merge (s1,s2) =
3.33 if s1 = s2
3.34 then s1
3.35 else error "Trying to merge two different import segments"
3.36 @@ -38,42 +36,38 @@
3.37 val get_import_segment = ImportSegment.get
3.38 val set_import_segment = ImportSegment.put
3.39
3.40 -structure HOL4UNames = TheoryDataFun
3.41 +structure HOL4UNames = Theory_Data
3.42 (
3.43 type T = string list
3.44 val empty = []
3.45 - val copy = I
3.46 val extend = I
3.47 - fun merge _ ([],[]) = []
3.48 - | merge _ _ = error "Used names not empty during merge"
3.49 + fun merge ([], []) = []
3.50 + | merge _ = error "Used names not empty during merge"
3.51 )
3.52
3.53 -structure HOL4Dump = TheoryDataFun
3.54 +structure HOL4Dump = Theory_Data
3.55 (
3.56 type T = string * string * string list
3.57 val empty = ("","",[])
3.58 - val copy = I
3.59 val extend = I
3.60 - fun merge _ (("","",[]),("","",[])) = ("","",[])
3.61 - | merge _ _ = error "Dump data not empty during merge"
3.62 + fun merge (("","",[]),("","",[])) = ("","",[])
3.63 + | merge _ = error "Dump data not empty during merge"
3.64 )
3.65
3.66 -structure HOL4Moves = TheoryDataFun
3.67 +structure HOL4Moves = Theory_Data
3.68 (
3.69 type T = string Symtab.table
3.70 val empty = Symtab.empty
3.71 - val copy = I
3.72 val extend = I
3.73 - fun merge _ : T * T -> T = Symtab.merge (K true)
3.74 + fun merge data = Symtab.merge (K true) data
3.75 )
3.76
3.77 -structure HOL4Imports = TheoryDataFun
3.78 +structure HOL4Imports = Theory_Data
3.79 (
3.80 type T = string Symtab.table
3.81 val empty = Symtab.empty
3.82 - val copy = I
3.83 val extend = I
3.84 - fun merge _ : T * T -> T = Symtab.merge (K true)
3.85 + fun merge data = Symtab.merge (K true) data
3.86 )
3.87
3.88 fun get_segment2 thyname thy =
3.89 @@ -87,85 +81,76 @@
3.90 HOL4Imports.put imps' thy
3.91 end
3.92
3.93 -structure HOL4CMoves = TheoryDataFun
3.94 +structure HOL4CMoves = Theory_Data
3.95 (
3.96 type T = string Symtab.table
3.97 val empty = Symtab.empty
3.98 - val copy = I
3.99 val extend = I
3.100 - fun merge _ : T * T -> T = Symtab.merge (K true)
3.101 + fun merge data = Symtab.merge (K true) data
3.102 )
3.103
3.104 -structure HOL4Maps = TheoryDataFun
3.105 +structure HOL4Maps = Theory_Data
3.106 (
3.107 - type T = (string option) StringPair.table
3.108 + type T = string option StringPair.table
3.109 val empty = StringPair.empty
3.110 - val copy = I
3.111 val extend = I
3.112 - fun merge _ : T * T -> T = StringPair.merge (K true)
3.113 + fun merge data = StringPair.merge (K true) data
3.114 )
3.115
3.116 -structure HOL4Thms = TheoryDataFun
3.117 +structure HOL4Thms = Theory_Data
3.118 (
3.119 type T = holthm StringPair.table
3.120 val empty = StringPair.empty
3.121 - val copy = I
3.122 val extend = I
3.123 - fun merge _ : T * T -> T = StringPair.merge (K true)
3.124 + fun merge data = StringPair.merge (K true) data
3.125 )
3.126
3.127 -structure HOL4ConstMaps = TheoryDataFun
3.128 +structure HOL4ConstMaps = Theory_Data
3.129 (
3.130 type T = (bool * string * typ option) StringPair.table
3.131 val empty = StringPair.empty
3.132 - val copy = I
3.133 val extend = I
3.134 - fun merge _ : T * T -> T = StringPair.merge (K true)
3.135 + fun merge data = StringPair.merge (K true) data
3.136 )
3.137
3.138 -structure HOL4Rename = TheoryDataFun
3.139 +structure HOL4Rename = Theory_Data
3.140 (
3.141 type T = string StringPair.table
3.142 val empty = StringPair.empty
3.143 - val copy = I
3.144 val extend = I
3.145 - fun merge _ : T * T -> T = StringPair.merge (K true)
3.146 + fun merge data = StringPair.merge (K true) data
3.147 )
3.148
3.149 -structure HOL4DefMaps = TheoryDataFun
3.150 +structure HOL4DefMaps = Theory_Data
3.151 (
3.152 type T = string StringPair.table
3.153 val empty = StringPair.empty
3.154 - val copy = I
3.155 val extend = I
3.156 - fun merge _ : T * T -> T = StringPair.merge (K true)
3.157 + fun merge data = StringPair.merge (K true) data
3.158 )
3.159
3.160 -structure HOL4TypeMaps = TheoryDataFun
3.161 +structure HOL4TypeMaps = Theory_Data
3.162 (
3.163 type T = (bool * string) StringPair.table
3.164 val empty = StringPair.empty
3.165 - val copy = I
3.166 val extend = I
3.167 - fun merge _ : T * T -> T = StringPair.merge (K true)
3.168 + fun merge data = StringPair.merge (K true) data
3.169 )
3.170
3.171 -structure HOL4Pending = TheoryDataFun
3.172 +structure HOL4Pending = Theory_Data
3.173 (
3.174 type T = ((term * term) list * thm) StringPair.table
3.175 val empty = StringPair.empty
3.176 - val copy = I
3.177 val extend = I
3.178 - fun merge _ : T * T -> T = StringPair.merge (K true)
3.179 + fun merge data = StringPair.merge (K true) data
3.180 )
3.181
3.182 -structure HOL4Rewrites = TheoryDataFun
3.183 +structure HOL4Rewrites = Theory_Data
3.184 (
3.185 type T = thm list
3.186 val empty = []
3.187 - val copy = I
3.188 val extend = I
3.189 - fun merge _ = Library.merge Thm.eq_thm_prop
3.190 + val merge = Thm.merge_thms
3.191 )
3.192
3.193 val hol4_debug = Unsynchronized.ref false
4.1 --- a/src/HOL/Import/import.ML Sun Nov 08 18:43:22 2009 +0100
4.2 +++ b/src/HOL/Import/import.ML Sun Nov 08 18:43:42 2009 +0100
4.3 @@ -9,13 +9,12 @@
4.4 val setup : theory -> theory
4.5 end
4.6
4.7 -structure ImportData = TheoryDataFun
4.8 +structure ImportData = Theory_Data
4.9 (
4.10 - type T = ProofKernel.thm option array option
4.11 + type T = ProofKernel.thm option array option (* FIXME mutable array !??!!! *)
4.12 val empty = NONE
4.13 - val copy = I
4.14 val extend = I
4.15 - fun merge _ _ = NONE
4.16 + fun merge _ = NONE
4.17 )
4.18
4.19 structure Import :> IMPORT =
5.1 --- a/src/HOL/Import/shuffler.ML Sun Nov 08 18:43:22 2009 +0100
5.2 +++ b/src/HOL/Import/shuffler.ML Sun Nov 08 18:43:42 2009 +0100
5.3 @@ -72,13 +72,12 @@
5.4 | _ => raise THM("Not an equality",0,[th]))
5.5 handle _ => raise THM("Couldn't make object equality",0,[th]) (* FIXME avoid handle _ *)
5.6
5.7 -structure ShuffleData = TheoryDataFun
5.8 +structure ShuffleData = Theory_Data
5.9 (
5.10 type T = thm list
5.11 val empty = []
5.12 - val copy = I
5.13 val extend = I
5.14 - fun merge _ = Library.merge Thm.eq_thm_prop
5.15 + val merge = Thm.merge_thms
5.16 )
5.17
5.18 fun print_shuffles thy =
6.1 --- a/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Nov 08 18:43:22 2009 +0100
6.2 +++ b/src/HOL/Mirabelle/Tools/mirabelle.ML Sun Nov 08 18:43:42 2009 +0100
6.3 @@ -60,13 +60,12 @@
6.4 type run_action = int -> run_args -> unit
6.5 type action = init_action * run_action * done_action
6.6
6.7 -structure Actions = TheoryDataFun
6.8 +structure Actions = Theory_Data
6.9 (
6.10 type T = (int * run_action * done_action) list
6.11 val empty = []
6.12 - val copy = I
6.13 val extend = I
6.14 - fun merge _ = Library.merge (K true)
6.15 + fun merge data = Library.merge (K true) data (* FIXME ?!? *)
6.16 )
6.17
6.18
7.1 --- a/src/HOL/Nominal/nominal_atoms.ML Sun Nov 08 18:43:22 2009 +0100
7.2 +++ b/src/HOL/Nominal/nominal_atoms.ML Sun Nov 08 18:43:42 2009 +0100
7.3 @@ -42,13 +42,12 @@
7.4 cp_inst : thm Symtab.table,
7.5 dj_thms : thm Symtab.table};
7.6
7.7 -structure NominalData = TheoryDataFun
7.8 +structure NominalData = Theory_Data
7.9 (
7.10 type T = atom_info Symtab.table;
7.11 val empty = Symtab.empty;
7.12 - val copy = I;
7.13 val extend = I;
7.14 - fun merge _ x = Symtab.merge (K true) x;
7.15 + fun merge data = Symtab.merge (K true) data;
7.16 );
7.17
7.18 fun make_atom_info ((((((pt_class, fs_class), cp_classes), at_inst), pt_inst), cp_inst), dj_thms) =
8.1 --- a/src/HOL/Nominal/nominal_datatype.ML Sun Nov 08 18:43:22 2009 +0100
8.2 +++ b/src/HOL/Nominal/nominal_datatype.ML Sun Nov 08 18:43:42 2009 +0100
8.3 @@ -84,13 +84,12 @@
8.4 distinct : thm list,
8.5 inject : thm list};
8.6
8.7 -structure NominalDatatypesData = TheoryDataFun
8.8 +structure NominalDatatypesData = Theory_Data
8.9 (
8.10 type T = nominal_datatype_info Symtab.table;
8.11 val empty = Symtab.empty;
8.12 - val copy = I;
8.13 val extend = I;
8.14 - fun merge _ tabs : T = Symtab.merge (K true) tabs;
8.15 + fun merge data = Symtab.merge (K true) data;
8.16 );
8.17
8.18 val get_nominal_datatypes = NominalDatatypesData.get;
9.1 --- a/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Nov 08 18:43:22 2009 +0100
9.2 +++ b/src/HOL/Tools/ATP_Manager/atp_manager.ML Sun Nov 08 18:43:42 2009 +0100
9.3 @@ -226,13 +226,12 @@
9.4
9.5 fun err_dup_prover name = error ("Duplicate prover: " ^ quote name);
9.6
9.7 -structure Provers = TheoryDataFun
9.8 +structure Provers = Theory_Data
9.9 (
9.10 type T = (ATP_Wrapper.prover * stamp) Symtab.table;
9.11 val empty = Symtab.empty;
9.12 - val copy = I;
9.13 val extend = I;
9.14 - fun merge _ tabs : T = Symtab.merge (eq_snd op =) tabs
9.15 + fun merge data : T = Symtab.merge (eq_snd op =) data
9.16 handle Symtab.DUP dup => err_dup_prover dup;
9.17 );
9.18
10.1 --- a/src/HOL/Tools/Datatype/datatype.ML Sun Nov 08 18:43:22 2009 +0100
10.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Sun Nov 08 18:43:42 2009 +0100
10.3 @@ -42,7 +42,7 @@
10.4
10.5 (* data management *)
10.6
10.7 -structure DatatypesData = TheoryDataFun
10.8 +structure DatatypesData = Theory_Data
10.9 (
10.10 type T =
10.11 {types: info Symtab.table,
10.12 @@ -51,11 +51,10 @@
10.13
10.14 val empty =
10.15 {types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
10.16 - val copy = I;
10.17 val extend = I;
10.18 - fun merge _
10.19 + fun merge
10.20 ({types = types1, constrs = constrs1, cases = cases1},
10.21 - {types = types2, constrs = constrs2, cases = cases2}) =
10.22 + {types = types2, constrs = constrs2, cases = cases2}) : T =
10.23 {types = Symtab.merge (K true) (types1, types2),
10.24 constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
10.25 cases = Symtab.merge (K true) (cases1, cases2)};
11.1 --- a/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Nov 08 18:43:22 2009 +0100
11.2 +++ b/src/HOL/Tools/Function/scnp_reconstruct.ML Sun Nov 08 18:43:42 2009 +0100
11.3 @@ -63,13 +63,12 @@
11.4 reduction_pair : thm
11.5 }
11.6
11.7 -structure Multiset_Setup = TheoryDataFun
11.8 +structure Multiset_Setup = Theory_Data
11.9 (
11.10 type T = multiset_setup option
11.11 val empty = NONE
11.12 - val copy = I;
11.13 val extend = I;
11.14 - fun merge _ (v1, v2) = if is_some v2 then v2 else v1
11.15 + fun merge (v1, v2) = if is_some v2 then v2 else v1 (* FIXME prefer v1 !?! *)
11.16 )
11.17
11.18 val multiset_setup = Multiset_Setup.put o SOME
12.1 --- a/src/HOL/Tools/Function/size.ML Sun Nov 08 18:43:22 2009 +0100
12.2 +++ b/src/HOL/Tools/Function/size.ML Sun Nov 08 18:43:42 2009 +0100
12.3 @@ -15,13 +15,12 @@
12.4
12.5 open DatatypeAux;
12.6
12.7 -structure SizeData = TheoryDataFun
12.8 +structure SizeData = Theory_Data
12.9 (
12.10 type T = (string * thm list) Symtab.table;
12.11 val empty = Symtab.empty;
12.12 - val copy = I
12.13 val extend = I
12.14 - fun merge _ = Symtab.merge (K true);
12.15 + fun merge data = Symtab.merge (K true) data;
12.16 );
12.17
12.18 val lookup_size = SizeData.get #> Symtab.lookup;
13.1 --- a/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Nov 08 18:43:22 2009 +0100
13.2 +++ b/src/HOL/Tools/Nitpick/nitpick_hol.ML Sun Nov 08 18:43:42 2009 +0100
13.3 @@ -179,14 +179,13 @@
13.4 unrolled_preds: unrolled list Unsynchronized.ref,
13.5 wf_cache: wf_cache Unsynchronized.ref}
13.6
13.7 -structure TheoryData = TheoryDataFun(
13.8 +structure TheoryData = Theory_Data(
13.9 type T = {frac_types: (string * (string * string) list) list,
13.10 codatatypes: (string * (string * styp list)) list}
13.11 val empty = {frac_types = [], codatatypes = []}
13.12 - val copy = I
13.13 val extend = I
13.14 - fun merge _ ({frac_types = fs1, codatatypes = cs1},
13.15 - {frac_types = fs2, codatatypes = cs2}) =
13.16 + fun merge ({frac_types = fs1, codatatypes = cs1},
13.17 + {frac_types = fs2, codatatypes = cs2}) : T =
13.18 {frac_types = AList.merge (op =) (op =) (fs1, fs2),
13.19 codatatypes = AList.merge (op =) (op =) (cs1, cs2)})
13.20
14.1 --- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Nov 08 18:43:22 2009 +0100
14.2 +++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Sun Nov 08 18:43:42 2009 +0100
14.3 @@ -125,13 +125,12 @@
14.4 | _ => value)
14.5 | NONE => (name, value)
14.6
14.7 -structure TheoryData = TheoryDataFun(
14.8 +structure TheoryData = Theory_Data(
14.9 type T = {params: raw_param list, registered_auto: bool}
14.10 val empty = {params = rev default_default_params, registered_auto = false}
14.11 - val copy = I
14.12 val extend = I
14.13 - fun merge _ ({params = ps1, registered_auto = a1},
14.14 - {params = ps2, registered_auto = a2}) =
14.15 + fun merge ({params = ps1, registered_auto = a1},
14.16 + {params = ps2, registered_auto = a2}) : T =
14.17 {params = AList.merge (op =) (op =) (ps1, ps2),
14.18 registered_auto = a1 orelse a2})
14.19
15.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Nov 08 18:43:22 2009 +0100
15.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Sun Nov 08 18:43:42 2009 +0100
15.3 @@ -232,13 +232,12 @@
15.4 eq_option (Thm.eq_thm) (#elim d1, #elim d2) andalso
15.5 #nparams d1 = #nparams d2
15.6
15.7 -structure PredData = TheoryDataFun
15.8 +structure PredData = Theory_Data
15.9 (
15.10 type T = pred_data Graph.T;
15.11 val empty = Graph.empty;
15.12 - val copy = I;
15.13 val extend = I;
15.14 - fun merge _ = Graph.merge eq_pred_data;
15.15 + val merge = Graph.merge eq_pred_data;
15.16 );
15.17
15.18 (* queries *)
15.19 @@ -2450,7 +2449,7 @@
15.20 (*FIXME name discrepancy in attribs and ML code*)
15.21 (*FIXME intros should be better named intro*)
15.22
15.23 -(* TODO: make TheoryDataFun to Generic_Data & remove duplication of local theory and theory *)
15.24 +(* TODO: make Theory_Data to Generic_Data & remove duplication of local theory and theory *)
15.25 fun generic_code_pred prep_const options raw_const lthy =
15.26 let
15.27 val thy = ProofContext.theory_of lthy
16.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Nov 08 18:43:22 2009 +0100
16.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_data.ML Sun Nov 08 18:43:42 2009 +0100
16.3 @@ -19,15 +19,14 @@
16.4
16.5 open Predicate_Compile_Aux;
16.6
16.7 -structure Data = TheoryDataFun
16.8 +structure Data = Theory_Data
16.9 (
16.10 type T =
16.11 {const_spec_table : thm list Symtab.table};
16.12 val empty =
16.13 {const_spec_table = Symtab.empty};
16.14 - val copy = I;
16.15 val extend = I;
16.16 - fun merge _
16.17 + fun merge
16.18 ({const_spec_table = const_spec_table1},
16.19 {const_spec_table = const_spec_table2}) =
16.20 {const_spec_table = Symtab.merge (K true) (const_spec_table1, const_spec_table2)}
17.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sun Nov 08 18:43:22 2009 +0100
17.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_fun.ML Sun Nov 08 18:43:42 2009 +0100
17.3 @@ -56,13 +56,12 @@
17.4 fun is_constr thy = is_some o Code.get_datatype_of_constr thy;
17.5
17.6 (* Table from constant name (string) to term of inductive predicate *)
17.7 -structure Pred_Compile_Preproc = TheoryDataFun
17.8 +structure Pred_Compile_Preproc = Theory_Data
17.9 (
17.10 type T = string Symtab.table;
17.11 val empty = Symtab.empty;
17.12 - val copy = I;
17.13 val extend = I;
17.14 - fun merge _ = Symtab.merge (op =);
17.15 + fun merge data : T = Symtab.merge (op =) data; (* FIXME handle Symtab.DUP ?? *)
17.16 )
17.17
17.18 fun pred_of_function thy name = Symtab.lookup (Pred_Compile_Preproc.get thy) name
18.1 --- a/src/HOL/Tools/arith_data.ML Sun Nov 08 18:43:22 2009 +0100
18.2 +++ b/src/HOL/Tools/arith_data.ML Sun Nov 08 18:43:42 2009 +0100
18.3 @@ -41,13 +41,12 @@
18.4
18.5 val get_arith_facts = Arith_Facts.get;
18.6
18.7 -structure Arith_Tactics = TheoryDataFun
18.8 +structure Arith_Tactics = Theory_Data
18.9 (
18.10 type T = (serial * (string * (bool -> Proof.context -> int -> tactic))) list;
18.11 val empty = [];
18.12 - val copy = I;
18.13 val extend = I;
18.14 - fun merge _ = AList.merge (op =) (K true);
18.15 + fun merge data : T = AList.merge (op =) (K true) data;
18.16 );
18.17
18.18 fun add_tactic name tac = Arith_Tactics.map (cons (serial (), (name, tac)));
19.1 --- a/src/HOL/Tools/inductive_codegen.ML Sun Nov 08 18:43:22 2009 +0100
19.2 +++ b/src/HOL/Tools/inductive_codegen.ML Sun Nov 08 18:43:42 2009 +0100
19.3 @@ -20,7 +20,7 @@
19.4 fun merge_rules tabs =
19.5 Symtab.join (fn _ => AList.merge (Thm.eq_thm_prop) (K true)) tabs;
19.6
19.7 -structure CodegenData = TheoryDataFun
19.8 +structure CodegenData = Theory_Data
19.9 (
19.10 type T =
19.11 {intros : (thm * (string * int)) list Symtab.table,
19.12 @@ -28,10 +28,9 @@
19.13 eqns : (thm * string) list Symtab.table};
19.14 val empty =
19.15 {intros = Symtab.empty, graph = Graph.empty, eqns = Symtab.empty};
19.16 - val copy = I;
19.17 val extend = I;
19.18 - fun merge _ ({intros=intros1, graph=graph1, eqns=eqns1},
19.19 - {intros=intros2, graph=graph2, eqns=eqns2}) =
19.20 + fun merge ({intros=intros1, graph=graph1, eqns=eqns1},
19.21 + {intros=intros2, graph=graph2, eqns=eqns2}) : T =
19.22 {intros = merge_rules (intros1, intros2),
19.23 graph = Graph.merge (K true) (graph1, graph2),
19.24 eqns = merge_rules (eqns1, eqns2)};
20.1 --- a/src/HOL/Tools/recdef.ML Sun Nov 08 18:43:22 2009 +0100
20.2 +++ b/src/HOL/Tools/recdef.ML Sun Nov 08 18:43:42 2009 +0100
20.3 @@ -86,18 +86,17 @@
20.4
20.5 type recdef_info = {simps: thm list, rules: thm list list, induct: thm, tcs: term list};
20.6
20.7 -structure GlobalRecdefData = TheoryDataFun
20.8 +structure GlobalRecdefData = Theory_Data
20.9 (
20.10 type T = recdef_info Symtab.table * hints;
20.11 val empty = (Symtab.empty, mk_hints ([], [], [])): T;
20.12 - val copy = I;
20.13 val extend = I;
20.14 - fun merge _
20.15 + fun merge
20.16 ((tab1, {simps = simps1, congs = congs1, wfs = wfs1}),
20.17 (tab2, {simps = simps2, congs = congs2, wfs = wfs2})) : T =
20.18 (Symtab.merge (K true) (tab1, tab2),
20.19 mk_hints (Thm.merge_thms (simps1, simps2),
20.20 - AList.merge (op =) Thm.eq_thm (congs1, congs2),
20.21 + AList.merge (op =) Thm.eq_thm_prop (congs1, congs2),
20.22 Thm.merge_thms (wfs1, wfs2)));
20.23 );
20.24
21.1 --- a/src/HOL/Tools/recfun_codegen.ML Sun Nov 08 18:43:22 2009 +0100
21.2 +++ b/src/HOL/Tools/recfun_codegen.ML Sun Nov 08 18:43:42 2009 +0100
21.3 @@ -16,13 +16,12 @@
21.4
21.5 val const_of = dest_Const o head_of o fst o Logic.dest_equals;
21.6
21.7 -structure ModuleData = TheoryDataFun
21.8 +structure ModuleData = Theory_Data
21.9 (
21.10 type T = string Symtab.table;
21.11 val empty = Symtab.empty;
21.12 - val copy = I;
21.13 val extend = I;
21.14 - fun merge _ = Symtab.merge (K true);
21.15 + fun merge data = Symtab.merge (K true) data;
21.16 );
21.17
21.18 fun add_thm_target module_name thm thy =
22.1 --- a/src/HOL/Tools/record.ML Sun Nov 08 18:43:22 2009 +0100
22.2 +++ b/src/HOL/Tools/record.ML Sun Nov 08 18:43:42 2009 +0100
22.3 @@ -81,13 +81,12 @@
22.4 cterm_instantiate (map (apfst getvar) values) thm
22.5 end;
22.6
22.7 -structure IsTupleThms = TheoryDataFun
22.8 +structure IsTupleThms = Theory_Data
22.9 (
22.10 type T = thm Symtab.table;
22.11 val empty = Symtab.make [tuple_istuple];
22.12 - val copy = I;
22.13 val extend = I;
22.14 - fun merge _ = Symtab.merge Thm.eq_thm_prop;
22.15 + fun merge data = Symtab.merge Thm.eq_thm_prop data; (* FIXME handle Symtab.DUP ?? *)
22.16 );
22.17
22.18 fun do_typedef name repT alphas thy =
22.19 @@ -381,7 +380,7 @@
22.20 equalities = equalities, extinjects=extinjects, extsplit = extsplit, splits = splits,
22.21 extfields = extfields, fieldext = fieldext }: record_data;
22.22
22.23 -structure RecordsData = TheoryDataFun
22.24 +structure RecordsData = Theory_Data
22.25 (
22.26 type T = record_data;
22.27 val empty =
22.28 @@ -390,10 +389,8 @@
22.29 simpset = HOL_basic_ss, defset = HOL_basic_ss,
22.30 foldcong = HOL_basic_ss, unfoldcong = HOL_basic_ss}
22.31 Symtab.empty [] Symtab.empty Symtab.empty Symtab.empty Symtab.empty;
22.32 -
22.33 - val copy = I;
22.34 val extend = I;
22.35 - fun merge _
22.36 + fun merge
22.37 ({records = recs1,
22.38 sel_upd =
22.39 {selectors = sels1, updates = upds1,
22.40 @@ -425,7 +422,7 @@
22.41 foldcong = Simplifier.merge_ss (fc1, fc2),
22.42 unfoldcong = Simplifier.merge_ss (uc1, uc2)}
22.43 (Symtab.merge Thm.eq_thm_prop (equalities1, equalities2))
22.44 - (Library.merge Thm.eq_thm_prop (extinjects1, extinjects2))
22.45 + (Thm.merge_thms (extinjects1, extinjects2))
22.46 (Symtab.merge Thm.eq_thm_prop (extsplit1, extsplit2))
22.47 (Symtab.merge (fn ((a, b, c, d), (w, x, y, z)) =>
22.48 Thm.eq_thm (a, w) andalso Thm.eq_thm (b, x) andalso
23.1 --- a/src/HOL/Tools/refute.ML Sun Nov 08 18:43:22 2009 +0100
23.2 +++ b/src/HOL/Tools/refute.ML Sun Nov 08 18:43:42 2009 +0100
23.3 @@ -201,7 +201,7 @@
23.4 };
23.5
23.6
23.7 - structure RefuteData = TheoryDataFun
23.8 + structure RefuteData = Theory_Data
23.9 (
23.10 type T =
23.11 {interpreters: (string * (theory -> model -> arguments -> term ->
23.12 @@ -210,11 +210,10 @@
23.13 (int -> bool) -> term option)) list,
23.14 parameters: string Symtab.table};
23.15 val empty = {interpreters = [], printers = [], parameters = Symtab.empty};
23.16 - val copy = I;
23.17 val extend = I;
23.18 - fun merge _
23.19 + fun merge
23.20 ({interpreters = in1, printers = pr1, parameters = pa1},
23.21 - {interpreters = in2, printers = pr2, parameters = pa2}) =
23.22 + {interpreters = in2, printers = pr2, parameters = pa2}) : T =
23.23 {interpreters = AList.merge (op =) (K true) (in1, in2),
23.24 printers = AList.merge (op =) (K true) (pr1, pr2),
23.25 parameters = Symtab.merge (op=) (pa1, pa2)};
24.1 --- a/src/HOL/Tools/res_axioms.ML Sun Nov 08 18:43:22 2009 +0100
24.2 +++ b/src/HOL/Tools/res_axioms.ML Sun Nov 08 18:43:42 2009 +0100
24.3 @@ -349,13 +349,12 @@
24.4
24.5 (*The cache prevents repeated clausification of a theorem, and also repeated declaration of
24.6 Skolem functions.*)
24.7 -structure ThmCache = TheoryDataFun
24.8 +structure ThmCache = Theory_Data
24.9 (
24.10 type T = thm list Thmtab.table * unit Symtab.table;
24.11 val empty = (Thmtab.empty, Symtab.empty);
24.12 - val copy = I;
24.13 val extend = I;
24.14 - fun merge _ ((cache1, seen1), (cache2, seen2)) : T =
24.15 + fun merge ((cache1, seen1), (cache2, seen2)) : T =
24.16 (Thmtab.merge (K true) (cache1, cache2), Symtab.merge (K true) (seen1, seen2));
24.17 );
24.18
25.1 --- a/src/HOL/Tools/typecopy.ML Sun Nov 08 18:43:22 2009 +0100
25.2 +++ b/src/HOL/Tools/typecopy.ML Sun Nov 08 18:43:42 2009 +0100
25.3 @@ -30,13 +30,12 @@
25.4 proj_def: thm
25.5 };
25.6
25.7 -structure TypecopyData = TheoryDataFun
25.8 +structure TypecopyData = Theory_Data
25.9 (
25.10 type T = info Symtab.table;
25.11 val empty = Symtab.empty;
25.12 - val copy = I;
25.13 val extend = I;
25.14 - fun merge _ = Symtab.merge (K true);
25.15 + fun merge data = Symtab.merge (K true) data;
25.16 );
25.17
25.18 val get_info = Symtab.lookup o TypecopyData.get;
26.1 --- a/src/HOL/Tools/typedef.ML Sun Nov 08 18:43:22 2009 +0100
26.2 +++ b/src/HOL/Tools/typedef.ML Sun Nov 08 18:43:42 2009 +0100
26.3 @@ -36,13 +36,12 @@
26.4 Abs_inverse: thm, Rep_inject: thm, Abs_inject: thm, Rep_cases: thm, Abs_cases: thm,
26.5 Rep_induct: thm, Abs_induct: thm};
26.6
26.7 -structure TypedefData = TheoryDataFun
26.8 +structure TypedefData = Theory_Data
26.9 (
26.10 type T = info Symtab.table;
26.11 val empty = Symtab.empty;
26.12 - val copy = I;
26.13 val extend = I;
26.14 - fun merge _ tabs : T = Symtab.merge (K true) tabs;
26.15 + fun merge data = Symtab.merge (K true) data;
26.16 );
26.17
26.18 val get_info = Symtab.lookup o TypedefData.get;
27.1 --- a/src/HOLCF/Tools/fixrec.ML Sun Nov 08 18:43:22 2009 +0100
27.2 +++ b/src/HOLCF/Tools/fixrec.ML Sun Nov 08 18:43:42 2009 +0100
27.3 @@ -252,12 +252,12 @@
27.4 (*********** monadic notation and pattern matching compilation ***********)
27.5 (*************************************************************************)
27.6
27.7 -structure FixrecMatchData = TheoryDataFun (
27.8 +structure FixrecMatchData = Theory_Data
27.9 +(
27.10 type T = string Symtab.table;
27.11 val empty = Symtab.empty;
27.12 - val copy = I;
27.13 val extend = I;
27.14 - fun merge _ = Symtab.merge (K true);
27.15 + fun merge data = Symtab.merge (K true) data;
27.16 );
27.17
27.18 (* associate match functions with pattern constants *)
27.19 @@ -523,8 +523,7 @@
27.20 end;
27.21
27.22 val setup =
27.23 - FixrecMatchData.init
27.24 - #> Attrib.setup @{binding fixrec_simp}
27.25 + Attrib.setup @{binding fixrec_simp}
27.26 (Attrib.add_del fixrec_simp_add fixrec_simp_del)
27.27 "declaration of fixrec simp rule"
27.28 #> Method.setup @{binding fixrec_simp}
28.1 --- a/src/Provers/classical.ML Sun Nov 08 18:43:22 2009 +0100
28.2 +++ b/src/Provers/classical.ML Sun Nov 08 18:43:42 2009 +0100
28.3 @@ -835,13 +835,12 @@
28.4
28.5 (* global clasets *)
28.6
28.7 -structure GlobalClaset = TheoryDataFun
28.8 +structure GlobalClaset = Theory_Data
28.9 (
28.10 type T = claset * context_cs;
28.11 val empty = (empty_cs, empty_context_cs);
28.12 - val copy = I;
28.13 val extend = I;
28.14 - fun merge _ ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
28.15 + fun merge ((cs1, ctxt_cs1), (cs2, ctxt_cs2)) =
28.16 (merge_cs (cs1, cs2), merge_context_cs (ctxt_cs1, ctxt_cs2));
28.17 );
28.18
29.1 --- a/src/Pure/Isar/attrib.ML Sun Nov 08 18:43:22 2009 +0100
29.2 +++ b/src/Pure/Isar/attrib.ML Sun Nov 08 18:43:42 2009 +0100
29.3 @@ -65,13 +65,12 @@
29.4
29.5 (* theory data *)
29.6
29.7 -structure Attributes = TheoryDataFun
29.8 +structure Attributes = Theory_Data
29.9 (
29.10 type T = ((src -> attribute) * string) Name_Space.table;
29.11 val empty : T = Name_Space.empty_table "attribute";
29.12 - val copy = I;
29.13 val extend = I;
29.14 - fun merge _ tables : T = Name_Space.merge_tables tables;
29.15 + fun merge data : T = Name_Space.merge_tables data;
29.16 );
29.17
29.18 fun print_attributes thy =
29.19 @@ -321,13 +320,12 @@
29.20
29.21 (* naming *)
29.22
29.23 -structure Configs = TheoryDataFun
29.24 +structure Configs = Theory_Data
29.25 (
29.26 type T = Config.value Config.T Symtab.table;
29.27 val empty = Symtab.empty;
29.28 - val copy = I;
29.29 val extend = I;
29.30 - fun merge _ = Symtab.merge (K true);
29.31 + fun merge data = Symtab.merge (K true) data;
29.32 );
29.33
29.34 fun print_configs ctxt =
30.1 --- a/src/Pure/Isar/class_target.ML Sun Nov 08 18:43:22 2009 +0100
30.2 +++ b/src/Pure/Isar/class_target.ML Sun Nov 08 18:43:42 2009 +0100
30.3 @@ -105,13 +105,12 @@
30.4 (Thm.merge_thms (defs1, defs2),
30.5 AList.merge (op =) (K true) (operations1, operations2)));
30.6
30.7 -structure ClassData = TheoryDataFun
30.8 +structure ClassData = Theory_Data
30.9 (
30.10 type T = class_data Graph.T
30.11 val empty = Graph.empty;
30.12 - val copy = I;
30.13 val extend = I;
30.14 - fun merge _ = Graph.join merge_class_data;
30.15 + val merge = Graph.join merge_class_data;
30.16 );
30.17
30.18
31.1 --- a/src/Pure/Isar/code.ML Sun Nov 08 18:43:22 2009 +0100
31.2 +++ b/src/Pure/Isar/code.ML Sun Nov 08 18:43:42 2009 +0100
31.3 @@ -703,13 +703,12 @@
31.4
31.5 (* c.f. src/HOL/Tools/recfun_codegen.ML *)
31.6
31.7 -structure Code_Target_Attr = TheoryDataFun (
31.8 +structure Code_Target_Attr = Theory_Data
31.9 +(
31.10 type T = (string -> thm -> theory -> theory) option;
31.11 val empty = NONE;
31.12 - val copy = I;
31.13 val extend = I;
31.14 - fun merge _ (NONE, f2) = f2
31.15 - | merge _ (f1, _) = f1;
31.16 + fun merge (f1, f2) = if is_some f1 then f1 else f2;
31.17 );
31.18
31.19 fun set_code_target_attr f = Code_Target_Attr.map (K (SOME f));
32.1 --- a/src/Pure/Isar/locale.ML Sun Nov 08 18:43:22 2009 +0100
32.2 +++ b/src/Pure/Isar/locale.ML Sun Nov 08 18:43:42 2009 +0100
32.3 @@ -122,13 +122,12 @@
32.4 merge (eq_snd op =) (notes, notes')),
32.5 merge (eq_snd op =) (dependencies, dependencies')));
32.6
32.7 -structure Locales = TheoryDataFun
32.8 +structure Locales = Theory_Data
32.9 (
32.10 type T = locale Name_Space.table;
32.11 val empty : T = Name_Space.empty_table "locale";
32.12 - val copy = I;
32.13 val extend = I;
32.14 - fun merge _ = Name_Space.join_tables (K merge_locale);
32.15 + val merge = Name_Space.join_tables (K merge_locale);
32.16 );
32.17
32.18 val intern = Name_Space.intern o #1 o Locales.get;
32.19 @@ -332,7 +331,7 @@
32.20
32.21 (*** Registrations: interpretations in theories ***)
32.22
32.23 -structure Registrations = TheoryDataFun
32.24 +structure Registrations = Theory_Data
32.25 (
32.26 type T = ((string * (morphism * morphism)) * stamp) list *
32.27 (* registrations, in reverse order of declaration *)
32.28 @@ -340,8 +339,7 @@
32.29 (* alist of mixin lists, per list mixins in reverse order of declaration *)
32.30 val empty = ([], []);
32.31 val extend = I;
32.32 - val copy = I;
32.33 - fun merge _ ((r1, m1), (r2, m2)) : T =
32.34 + fun merge ((r1, m1), (r2, m2)) : T =
32.35 (Library.merge (eq_snd op =) (r1, r2),
32.36 AList.join (op =) (K (Library.merge (eq_snd op =))) (m1, m2));
32.37 (* FIXME consolidate with dependencies, consider one data slot only *)
33.1 --- a/src/Pure/Isar/method.ML Sun Nov 08 18:43:22 2009 +0100
33.2 +++ b/src/Pure/Isar/method.ML Sun Nov 08 18:43:42 2009 +0100
33.3 @@ -320,13 +320,12 @@
33.4
33.5 (* method definitions *)
33.6
33.7 -structure Methods = TheoryDataFun
33.8 +structure Methods = Theory_Data
33.9 (
33.10 type T = ((src -> Proof.context -> method) * string) Name_Space.table;
33.11 val empty : T = Name_Space.empty_table "method";
33.12 - val copy = I;
33.13 val extend = I;
33.14 - fun merge _ tables : T = Name_Space.merge_tables tables;
33.15 + fun merge data : T = Name_Space.merge_tables data;
33.16 );
33.17
33.18 fun print_methods thy =
34.1 --- a/src/Pure/Isar/object_logic.ML Sun Nov 08 18:43:22 2009 +0100
34.2 +++ b/src/Pure/Isar/object_logic.ML Sun Nov 08 18:43:42 2009 +0100
34.3 @@ -47,18 +47,17 @@
34.4 fun make_data (base_sort, judgment, atomize_rulify) =
34.5 Data {base_sort = base_sort, judgment = judgment, atomize_rulify = atomize_rulify};
34.6
34.7 -structure ObjectLogicData = TheoryDataFun
34.8 +structure ObjectLogicData = Theory_Data
34.9 (
34.10 type T = data;
34.11 val empty = make_data (NONE, NONE, ([], []));
34.12 - val copy = I;
34.13 val extend = I;
34.14
34.15 fun merge_opt eq (SOME x, SOME y) =
34.16 if eq (x, y) then SOME x else error "Attempt to merge different object-logics"
34.17 | merge_opt _ (x, y) = if is_some x then x else y;
34.18
34.19 - fun merge _
34.20 + fun merge
34.21 (Data {base_sort = base_sort1, judgment = judgment1, atomize_rulify = (atomize1, rulify1)},
34.22 Data {base_sort = base_sort2, judgment = judgment2, atomize_rulify = (atomize2, rulify2)}) =
34.23 make_data (merge_opt (op =) (base_sort1, base_sort2), merge_opt (op =) (judgment1, judgment2),
35.1 --- a/src/Pure/Proof/extraction.ML Sun Nov 08 18:43:22 2009 +0100
35.2 +++ b/src/Pure/Proof/extraction.ML Sun Nov 08 18:43:42 2009 +0100
35.3 @@ -167,7 +167,7 @@
35.4
35.5 (* theory data *)
35.6
35.7 -structure ExtractionData = TheoryDataFun
35.8 +structure ExtractionData = Theory_Data
35.9 (
35.10 type T =
35.11 {realizes_eqns : rules,
35.12 @@ -187,20 +187,19 @@
35.13 defs = [],
35.14 expand = [],
35.15 prep = NONE};
35.16 - val copy = I;
35.17 val extend = I;
35.18
35.19 - fun merge _
35.20 - (({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
35.21 + fun merge
35.22 + ({realizes_eqns = realizes_eqns1, typeof_eqns = typeof_eqns1, types = types1,
35.23 realizers = realizers1, defs = defs1, expand = expand1, prep = prep1},
35.24 {realizes_eqns = realizes_eqns2, typeof_eqns = typeof_eqns2, types = types2,
35.25 - realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T * T) =
35.26 + realizers = realizers2, defs = defs2, expand = expand2, prep = prep2}) : T =
35.27 {realizes_eqns = merge_rules realizes_eqns1 realizes_eqns2,
35.28 typeof_eqns = merge_rules typeof_eqns1 typeof_eqns2,
35.29 types = AList.merge (op =) (K true) (types1, types2),
35.30 realizers = Symtab.merge_list (eq_set (op =) o pairself #1) (realizers1, realizers2),
35.31 defs = Library.merge Thm.eq_thm (defs1, defs2),
35.32 - expand = Library.merge (op =) (expand1, expand2),
35.33 + expand = Library.merge (op =) (expand1, expand2), (* FIXME proper aconv !?! *)
35.34 prep = (case prep1 of NONE => prep2 | _ => prep1)};
35.35 );
35.36
36.1 --- a/src/Pure/Thy/present.ML Sun Nov 08 18:43:22 2009 +0100
36.2 +++ b/src/Pure/Thy/present.ML Sun Nov 08 18:43:42 2009 +0100
36.3 @@ -64,13 +64,12 @@
36.4
36.5 (** additional theory data **)
36.6
36.7 -structure BrowserInfoData = TheoryDataFun
36.8 +structure BrowserInfoData = Theory_Data
36.9 (
36.10 type T = {name: string, session: string list, is_local: bool};
36.11 val empty = {name = "", session = [], is_local = false}: T;
36.12 - val copy = I;
36.13 fun extend _ = empty;
36.14 - fun merge _ _ = empty;
36.15 + fun merge _ = empty;
36.16 );
36.17
36.18 val put_info = BrowserInfoData.put;
37.1 --- a/src/Pure/Thy/term_style.ML Sun Nov 08 18:43:22 2009 +0100
37.2 +++ b/src/Pure/Thy/term_style.ML Sun Nov 08 18:43:42 2009 +0100
37.3 @@ -19,13 +19,12 @@
37.4 fun err_dup_style name =
37.5 error ("Duplicate declaration of antiquote style: " ^ quote name);
37.6
37.7 -structure StyleData = TheoryDataFun
37.8 +structure StyleData = Theory_Data
37.9 (
37.10 type T = ((Proof.context -> term -> term) parser * stamp) Symtab.table;
37.11 val empty = Symtab.empty;
37.12 - val copy = I;
37.13 val extend = I;
37.14 - fun merge _ tabs : T = Symtab.merge (eq_snd (op =)) tabs
37.15 + fun merge data : T = Symtab.merge (eq_snd (op =)) data
37.16 handle Symtab.DUP dup => err_dup_style dup;
37.17 );
37.18
38.1 --- a/src/Pure/Thy/thy_info.ML Sun Nov 08 18:43:22 2009 +0100
38.2 +++ b/src/Pure/Thy/thy_info.ML Sun Nov 08 18:43:42 2009 +0100
38.3 @@ -233,15 +233,14 @@
38.4
38.5 (* management data *)
38.6
38.7 -structure Management_Data = TheoryDataFun
38.8 +structure Management_Data = Theory_Data
38.9 (
38.10 type T =
38.11 Task_Queue.group option * (*worker thread group*)
38.12 int; (*abstract update time*)
38.13 val empty = (NONE, 0);
38.14 - val copy = I;
38.15 fun extend _ = empty;
38.16 - fun merge _ _ = empty;
38.17 + fun merge _ = empty;
38.18 );
38.19
38.20 val thy_ord = int_ord o pairself (#2 o Management_Data.get);
39.1 --- a/src/Pure/codegen.ML Sun Nov 08 18:43:22 2009 +0100
39.2 +++ b/src/Pure/codegen.ML Sun Nov 08 18:43:42 2009 +0100
39.3 @@ -185,7 +185,7 @@
39.4
39.5 (* theory data *)
39.6
39.7 -structure CodegenData = TheoryDataFun
39.8 +structure CodegenData = Theory_Data
39.9 (
39.10 type T =
39.11 {codegens : (string * term codegen) list,
39.12 @@ -198,16 +198,15 @@
39.13 val empty =
39.14 {codegens = [], tycodegens = [], consts = [], types = [],
39.15 preprocs = [], modules = Symtab.empty};
39.16 - val copy = I;
39.17 val extend = I;
39.18
39.19 - fun merge _
39.20 + fun merge
39.21 ({codegens = codegens1, tycodegens = tycodegens1,
39.22 consts = consts1, types = types1,
39.23 preprocs = preprocs1, modules = modules1} : T,
39.24 {codegens = codegens2, tycodegens = tycodegens2,
39.25 consts = consts2, types = types2,
39.26 - preprocs = preprocs2, modules = modules2}) =
39.27 + preprocs = preprocs2, modules = modules2}) : T =
39.28 {codegens = AList.merge (op =) (K true) (codegens1, codegens2),
39.29 tycodegens = AList.merge (op =) (K true) (tycodegens1, tycodegens2),
39.30 consts = AList.merge (op =) (K true) (consts1, consts2),
39.31 @@ -287,13 +286,12 @@
39.32 | _ => err ()
39.33 end;
39.34
39.35 -structure UnfoldData = TheoryDataFun
39.36 +structure UnfoldData = Theory_Data
39.37 (
39.38 type T = simpset;
39.39 val empty = empty_ss;
39.40 - val copy = I;
39.41 val extend = I;
39.42 - fun merge _ = merge_ss;
39.43 + val merge = merge_ss;
39.44 );
39.45
39.46 val map_unfold = UnfoldData.map;
40.1 --- a/src/Pure/interpretation.ML Sun Nov 08 18:43:22 2009 +0100
40.2 +++ b/src/Pure/interpretation.ML Sun Nov 08 18:43:42 2009 +0100
40.3 @@ -18,13 +18,12 @@
40.4
40.5 type T = T;
40.6
40.7 -structure Interp = TheoryDataFun
40.8 +structure Interp = Theory_Data
40.9 (
40.10 type T = T list * (((T -> theory -> theory) * stamp) * T list) list;
40.11 val empty = ([], []);
40.12 val extend = I;
40.13 - val copy = I;
40.14 - fun merge _ ((data1, interps1), (data2, interps2)) : T =
40.15 + fun merge ((data1, interps1), (data2, interps2)) : T =
40.16 (Library.merge eq (data1, data2),
40.17 AList.join (eq_snd (op =)) (K (Library.merge eq)) (interps1, interps2));
40.18 );
41.1 --- a/src/Pure/proofterm.ML Sun Nov 08 18:43:22 2009 +0100
41.2 +++ b/src/Pure/proofterm.ML Sun Nov 08 18:43:42 2009 +0100
41.3 @@ -1247,14 +1247,13 @@
41.4
41.5 (**** theory data ****)
41.6
41.7 -structure ProofData = TheoryDataFun
41.8 +structure ProofData = Theory_Data
41.9 (
41.10 type T = (stamp * (proof * proof)) list * (stamp * (typ list -> proof -> proof option)) list;
41.11
41.12 val empty = ([], []);
41.13 - val copy = I;
41.14 val extend = I;
41.15 - fun merge _ ((rules1, procs1), (rules2, procs2)) : T =
41.16 + fun merge ((rules1, procs1), (rules2, procs2)) : T =
41.17 (AList.merge (op =) (K true) (rules1, rules2),
41.18 AList.merge (op =) (K true) (procs1, procs2));
41.19 );
42.1 --- a/src/Pure/pure_thy.ML Sun Nov 08 18:43:22 2009 +0100
42.2 +++ b/src/Pure/pure_thy.ML Sun Nov 08 18:43:42 2009 +0100
42.3 @@ -54,13 +54,12 @@
42.4
42.5 (** theory data **)
42.6
42.7 -structure FactsData = TheoryDataFun
42.8 +structure FactsData = Theory_Data
42.9 (
42.10 type T = Facts.T * thm list;
42.11 val empty = (Facts.empty, []);
42.12 - val copy = I;
42.13 fun extend (facts, _) = (facts, []);
42.14 - fun merge _ ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
42.15 + fun merge ((facts1, _), (facts2, _)) = (Facts.merge (facts1, facts2), []);
42.16 );
42.17
42.18
42.19 @@ -246,13 +245,12 @@
42.20 ("_applC", typ "('b => 'a) => cargs => logic", Mixfix ("(1_/ _)", [1000, 1000], 999)),
42.21 ("_applC", typ "('b => 'a) => cargs => aprop", Mixfix ("(1_/ _)", [1000, 1000], 999))];
42.22
42.23 -structure OldApplSyntax = TheoryDataFun
42.24 +structure OldApplSyntax = Theory_Data
42.25 (
42.26 type T = bool;
42.27 val empty = false;
42.28 - val copy = I;
42.29 val extend = I;
42.30 - fun merge _ (b1, b2) : T =
42.31 + fun merge (b1, b2) : T =
42.32 if b1 = b2 then b1
42.33 else error "Cannot merge theories with different application syntax";
42.34 );
42.35 @@ -269,7 +267,7 @@
42.36
42.37 val _ = Context.>> (Context.map_theory
42.38 (Sign.map_naming (Name_Space.set_theory_name Context.PureN) #>
42.39 - OldApplSyntax.init #>
42.40 + OldApplSyntax.put false #>
42.41 Sign.add_types
42.42 [(Binding.name "fun", 2, NoSyn),
42.43 (Binding.name "prop", 0, NoSyn),
43.1 --- a/src/Pure/thm.ML Sun Nov 08 18:43:22 2009 +0100
43.2 +++ b/src/Pure/thm.ML Sun Nov 08 18:43:42 2009 +0100
43.3 @@ -1724,13 +1724,12 @@
43.4
43.5 (* authentic derivation names *)
43.6
43.7 -structure Oracles = TheoryDataFun
43.8 +structure Oracles = Theory_Data
43.9 (
43.10 type T = unit Name_Space.table;
43.11 val empty : T = Name_Space.empty_table "oracle";
43.12 - val copy = I;
43.13 val extend = I;
43.14 - fun merge _ oracles : T = Name_Space.merge_tables oracles;
43.15 + fun merge data : T = Name_Space.merge_tables data;
43.16 );
43.17
43.18 val extern_oracles = map #1 o Name_Space.extern_table o Oracles.get;
44.1 --- a/src/Tools/Code/code_preproc.ML Sun Nov 08 18:43:22 2009 +0100
44.2 +++ b/src/Tools/Code/code_preproc.ML Sun Nov 08 18:43:42 2009 +0100
44.3 @@ -56,13 +56,12 @@
44.4 val functrans = AList.merge (op =) (eq_fst (op =)) (functrans1, functrans2);
44.5 in make_thmproc ((pre, post), functrans) end;
44.6
44.7 -structure Code_Preproc_Data = TheoryDataFun
44.8 +structure Code_Preproc_Data = Theory_Data
44.9 (
44.10 type T = thmproc;
44.11 val empty = make_thmproc ((Simplifier.empty_ss, Simplifier.empty_ss), []);
44.12 - fun copy spec = spec;
44.13 - val extend = copy;
44.14 - fun merge _ = merge_thmproc;
44.15 + val extend = I;
44.16 + val merge = merge_thmproc;
44.17 );
44.18
44.19 fun the_thmproc thy = case Code_Preproc_Data.get thy
45.1 --- a/src/Tools/Code/code_target.ML Sun Nov 08 18:43:22 2009 +0100
45.2 +++ b/src/Tools/Code/code_target.ML Sun Nov 08 18:43:42 2009 +0100
45.3 @@ -148,13 +148,12 @@
45.4 else
45.5 error ("Incompatible serializers: " ^ quote target);
45.6
45.7 -structure CodeTargetData = TheoryDataFun
45.8 +structure CodeTargetData = Theory_Data
45.9 (
45.10 type T = target Symtab.table * string list;
45.11 val empty = (Symtab.empty, []);
45.12 - val copy = I;
45.13 val extend = I;
45.14 - fun merge _ ((target1, exc1) : T, (target2, exc2)) =
45.15 + fun merge ((target1, exc1), (target2, exc2)) : T =
45.16 (Symtab.join (merge_target true) (target1, target2), Library.merge (op =) (exc1, exc2));
45.17 );
45.18
46.1 --- a/src/Tools/nbe.ML Sun Nov 08 18:43:22 2009 +0100
46.2 +++ b/src/Tools/nbe.ML Sun Nov 08 18:43:42 2009 +0100
46.3 @@ -37,13 +37,12 @@
46.4
46.5 (** certificates and oracle for "trivial type classes" **)
46.6
46.7 -structure Triv_Class_Data = TheoryDataFun
46.8 +structure Triv_Class_Data = Theory_Data
46.9 (
46.10 type T = (class * thm) list;
46.11 val empty = [];
46.12 - val copy = I;
46.13 val extend = I;
46.14 - fun merge pp = AList.merge (op =) (K true);
46.15 + fun merge data : T = AList.merge (op =) (K true) data;
46.16 );
46.17
46.18 fun add_const_alias thm thy =
47.1 --- a/src/Tools/quickcheck.ML Sun Nov 08 18:43:22 2009 +0100
47.2 +++ b/src/Tools/quickcheck.ML Sun Nov 08 18:43:42 2009 +0100
47.3 @@ -52,16 +52,16 @@
47.4 make_test_params ((Int.max (size1, size2), Int.max (iterations1, iterations2)),
47.5 case default_type1 of NONE => default_type2 | _ => default_type1);
47.6
47.7 -structure Data = TheoryDataFun(
47.8 +structure Data = Theory_Data
47.9 +(
47.10 type T = (string * (Proof.context -> term -> int -> term list option)) list
47.11 * test_params;
47.12 val empty = ([], Test_Params { size = 10, iterations = 100, default_type = NONE });
47.13 - val copy = I;
47.14 val extend = I;
47.15 - fun merge pp ((generators1, params1), (generators2, params2)) =
47.16 - (AList.merge (op = : string * string -> bool) (K true) (generators1, generators2),
47.17 + fun merge ((generators1, params1), (generators2, params2)) : T =
47.18 + (AList.merge (op =) (K true) (generators1, generators2),
47.19 merge_test_params (params1, params2));
47.20 -)
47.21 +);
47.22
47.23 val add_generator = Data.map o apfst o AList.update (op =);
47.24
48.1 --- a/src/Tools/value.ML Sun Nov 08 18:43:22 2009 +0100
48.2 +++ b/src/Tools/value.ML Sun Nov 08 18:43:42 2009 +0100
48.3 @@ -15,12 +15,12 @@
48.4 structure Value : VALUE =
48.5 struct
48.6
48.7 -structure Evaluator = TheoryDataFun(
48.8 +structure Evaluator = Theory_Data
48.9 +(
48.10 type T = (string * (Proof.context -> term -> term)) list;
48.11 val empty = [];
48.12 - val copy = I;
48.13 val extend = I;
48.14 - fun merge _ data = AList.merge (op =) (K true) data;
48.15 + fun merge data : T = AList.merge (op =) (K true) data;
48.16 )
48.17
48.18 val add_evaluator = Evaluator.map o AList.update (op =);
49.1 --- a/src/ZF/Tools/ind_cases.ML Sun Nov 08 18:43:22 2009 +0100
49.2 +++ b/src/ZF/Tools/ind_cases.ML Sun Nov 08 18:43:42 2009 +0100
49.3 @@ -18,13 +18,12 @@
49.4
49.5 (* theory data *)
49.6
49.7 -structure IndCasesData = TheoryDataFun
49.8 +structure IndCasesData = Theory_Data
49.9 (
49.10 type T = (simpset -> cterm -> thm) Symtab.table;
49.11 val empty = Symtab.empty;
49.12 - val copy = I;
49.13 val extend = I;
49.14 - fun merge _ tabs : T = Symtab.merge (K true) tabs;
49.15 + fun merge data = Symtab.merge (K true) data;
49.16 );
49.17
49.18
50.1 --- a/src/ZF/Tools/induct_tacs.ML Sun Nov 08 18:43:22 2009 +0100
50.2 +++ b/src/ZF/Tools/induct_tacs.ML Sun Nov 08 18:43:42 2009 +0100
50.3 @@ -29,13 +29,12 @@
50.4 mutual_induct : thm,
50.5 exhaustion : thm};
50.6
50.7 -structure DatatypesData = TheoryDataFun
50.8 +structure DatatypesData = Theory_Data
50.9 (
50.10 type T = datatype_info Symtab.table;
50.11 val empty = Symtab.empty;
50.12 - val copy = I;
50.13 val extend = I;
50.14 - fun merge _ tabs : T = Symtab.merge (K true) tabs;
50.15 + fun merge data : T = Symtab.merge (K true) data;
50.16 );
50.17
50.18
50.19 @@ -49,13 +48,12 @@
50.20 rec_rewrites : thm list}; (*recursor equations*)
50.21
50.22
50.23 -structure ConstructorsData = TheoryDataFun
50.24 +structure ConstructorsData = Theory_Data
50.25 (
50.26 type T = constructor_info Symtab.table
50.27 val empty = Symtab.empty
50.28 - val copy = I;
50.29 val extend = I
50.30 - fun merge _ tabs : T = Symtab.merge (K true) tabs;
50.31 + fun merge data = Symtab.merge (K true) data;
50.32 );
50.33
50.34 structure DatatypeTactics : DATATYPE_TACTICS =