# HG changeset patch
# User wenzelm
# Date 1164892654 -3600
# Node ID 2ca27eeb2841e94e48c94846356e878d2f74f011
# Parent  3698319f6503e363928769f78e59d2ce0e491183
added merge_list;

diff -r 3698319f6503 -r 2ca27eeb2841 src/Pure/theory.ML
--- 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;