src/Pure/theory.ML
changeset 21608 2ca27eeb2841
parent 20549 c643984eb94b
child 21772 7c7ade4f537b
     1.1 --- a/src/Pure/theory.ML	Thu Nov 30 14:17:32 2006 +0100
     1.2 +++ b/src/Pure/theory.ML	Thu Nov 30 14:17:34 2006 +0100
     1.3 @@ -41,6 +41,7 @@
     1.4    val deref: theory_ref -> theory
     1.5    val merge: theory * theory -> theory                     (*exception TERM*)
     1.6    val merge_refs: theory_ref * theory_ref -> theory_ref    (*exception TERM*)
     1.7 +  val merge_list: theory list -> theory                    (*exception TERM*)
     1.8    val requires: theory -> string -> string -> unit
     1.9    val assert_super: theory -> theory -> theory
    1.10    val add_axioms: (bstring * string) list -> theory -> theory
    1.11 @@ -72,6 +73,9 @@
    1.12  val merge = Context.merge;
    1.13  val merge_refs = Context.merge_refs;
    1.14  
    1.15 +fun merge_list [] = raise TERM ("Empty merge of theories", [])
    1.16 +  | merge_list (thy :: thys) = Library.foldl merge (thy, thys);
    1.17 +
    1.18  val begin_theory = Sign.local_path oo Context.begin_thy Sign.pp;
    1.19  val end_theory = Context.finish_thy;
    1.20  val checkpoint = Context.checkpoint_thy;