--- a/src/Pure/theory.ML Thu Nov 30 14:17:32 2006 +0100
+++ b/src/Pure/theory.ML Thu Nov 30 14:17:34 2006 +0100
@@ -41,6 +41,7 @@
val deref: theory_ref -> theory
val merge: theory * theory -> theory (*exception TERM*)
val merge_refs: theory_ref * theory_ref -> theory_ref (*exception TERM*)
+ val merge_list: theory list -> theory (*exception TERM*)
val requires: theory -> string -> string -> unit
val assert_super: theory -> theory -> theory
val add_axioms: (bstring * string) list -> theory -> theory
@@ -72,6 +73,9 @@
val merge = Context.merge;
val merge_refs = Context.merge_refs;
+fun merge_list [] = raise TERM ("Empty merge of theories", [])
+ | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
+
val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp;
val end_theory = Context.finish_thy;
val checkpoint = Context.checkpoint_thy;