--- a/src/Pure/theory.ML Fri Aug 28 16:48:05 2015 +0200
+++ b/src/Pure/theory.ML Fri Aug 28 23:21:04 2015 +0200
@@ -9,8 +9,6 @@
val parents_of: theory -> theory list
val ancestors_of: theory -> theory list
val nodes_of: theory -> theory list
- val merge: theory * theory -> theory
- val merge_list: theory list -> theory
val setup: (theory -> theory) -> unit
val local_setup: (Proof.context -> Proof.context) -> unit
val get_markup: theory -> Markup.T
@@ -42,11 +40,6 @@
val ancestors_of = Context.ancestors_of;
fun nodes_of thy = thy :: ancestors_of thy;
-val merge = Context.merge;
-
-fun merge_list [] = raise THEORY ("Empty merge of theories", [])
- | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
-
fun setup f = Context.>> (Context.map_theory f);
fun local_setup f = Context.>> (Context.map_proof f);