# HG changeset patch
# User wenzelm
# Date 1005510849 -3600
# Node ID dc42d17c5b53acce58cd37ca5f0971a62a5a9f09
# Parent  c81ef8865cfb18537683480f9ddce9fd1b21c01e
added add_thmss;

diff -r c81ef8865cfb -r dc42d17c5b53 src/Pure/Isar/locale.ML
--- a/src/Pure/Isar/locale.ML	Sun Nov 11 21:33:40 2001 +0100
+++ b/src/Pure/Isar/locale.ML	Sun Nov 11 21:34:09 2001 +0100
@@ -39,7 +39,8 @@
   val activate_locale_i: string -> context -> context
   val add_locale: bstring -> xstring list -> context attribute element list -> theory -> theory
   val add_locale_i: bstring -> xstring list -> context attribute element_i list -> theory -> theory
-  val store_thm: string -> (string * thm) * context attribute list -> theory -> theory
+  val add_thmss: string -> ((string * thm list) * context attribute list) list
+    -> theory -> theory
   val setup: (theory -> theory) list
 end;
 
@@ -290,13 +291,15 @@
 
 (** store results **)
 
-fun store_thm name ((a, th), atts) thy =
+fun add_thmss name args thy =
   let
     val {imports, elements, closed} = the_locale thy name;
-    val note = Notes [((a, atts), [([Thm.name_thm (a, th)], [])])];
+    val _ = conditional closed (fn () =>
+      error ("Cannot store results in closed locale: " ^ quote name));
+    val note = Notes (map (fn ((a, ths), atts) =>
+      ((a, atts), [(map (curry Thm.name_thm a) ths, [])])) args);
   in
-    conditional closed (fn () => error ("Cannot store results in closed locale: " ^ quote name));
-    activate (ProofContext.init thy |> activate_locale_i name, note);    (*test attribute*)
+    activate (thy |> ProofContext.init |> activate_locale_i name, note);    (*test attributes!*)
     thy |> put_locale name (make_locale imports (elements @ [note]) closed)
   end;