# 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;