--- a/src/Pure/theory.ML Thu Apr 20 15:26:34 2023 +0200
+++ b/src/Pure/theory.ML Thu Apr 20 21:26:35 2023 +0200
@@ -22,7 +22,6 @@
val defs_of: theory -> Defs.T
val at_begin: (theory -> theory option) -> theory -> theory
val at_end: (theory -> theory option) -> theory -> theory
- val join_theory: theory list -> theory
val begin_theory: string * Position.T -> theory list -> theory
val end_theory: theory -> theory
val add_axiom: Proof.context -> binding * term -> theory -> theory
@@ -83,6 +82,8 @@
defs: Defs.T,
wrappers: wrapper list * wrapper list};
+fun rep_thy (Thy args) = args;
+
fun make_thy (pos, id, axioms, defs, wrappers) =
Thy {pos = pos, id = id, axioms = axioms, defs = defs, wrappers = wrappers};
@@ -90,19 +91,22 @@
(
type T = thy;
val empty = make_thy (Position.none, 0, Name_Space.empty_table Markup.axiomN, Defs.empty, ([], []));
- fun merge old_thys (thy1, thy2) =
+ fun merge args =
let
- val Thy {pos, id, axioms = axioms1, defs = defs1, wrappers = (bgs1, ens1)} = thy1;
- val Thy {pos = _, id = _, axioms = axioms2, defs = defs2, wrappers = (bgs2, ens2)} = thy2;
+ val thy0 = #1 (hd args);
+ val {pos, id, ...} = rep_thy (#2 (hd args));
- val axioms' = Name_Space.merge_tables (axioms1, axioms2);
- val defs' = Defs.merge (Defs.global_context (fst old_thys)) (defs1, defs2);
- val bgs' = Library.merge (eq_snd op =) (bgs1, bgs2);
- val ens' = Library.merge (eq_snd op =) (ens1, ens2);
+ val merge_defs = Defs.merge (Defs.global_context thy0);
+ val merge_wrappers = Library.merge (eq_snd op =);
+
+ val axioms' = Library.foldl1 Name_Space.merge_tables (map (#axioms o rep_thy o #2) args);
+ val defs' = Library.foldl1 merge_defs (map (#defs o rep_thy o #2) args);
+ val bgs' = Library.foldl1 merge_wrappers (map (#1 o #wrappers o rep_thy o #2) args);
+ val ens' = Library.foldl1 merge_wrappers (map (#2 o #wrappers o rep_thy o #2) args);
in make_thy (pos, id, axioms', defs', (bgs', ens')) end;
);
-fun rep_theory thy = Thy.get thy |> (fn Thy args => args);
+val rep_theory = rep_thy o Thy.get;
fun map_thy f = Thy.map (fn (Thy {pos, id, axioms, defs, wrappers}) =>
make_thy (f (pos, id, axioms, defs, wrappers)));
@@ -162,13 +166,6 @@
val defs_of = #defs o rep_theory;
-(* join theory *)
-
-fun join_theory [] = raise List.Empty
- | join_theory [thy] = thy
- | join_theory thys = foldl1 Context.join_thys thys;
-
-
(* begin/end theory *)
val begin_wrappers = rev o #1 o #wrappers o rep_theory;