# HG changeset patch
# User wenzelm
# Date 936212699 -7200
# Node ID 7e4e286a99314f914862c181cd41cfabd9352718
# Parent  e488cf3da60ae9119d9fa73e87189876e3f8216e
smart_store_thms;

diff -r e488cf3da60a -r 7e4e286a9931 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Wed Sep 01 21:04:01 1999 +0200
+++ b/src/Pure/pure_thy.ML	Wed Sep 01 21:04:59 1999 +0200
@@ -29,7 +29,7 @@
   val thms_containing: theory -> string list -> (string * thm) list
   val default_name: string -> string
   val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
-  val smart_store_thm: (bstring * thm) -> thm
+  val smart_store_thms: (bstring * thm list) -> thm list
   val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory
   val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory
   val have_thmss: bstring option -> theory attribute list ->
@@ -285,10 +285,15 @@
   in (thy', th') end;
 
 
-(* smart_store_thm *)
+(* smart_store_thms *)
 
-fun smart_store_thm (name, thm) =
-  hd (enter_thmx (Thm.sign_of_thm thm) name_single (name, thm));
+fun smart_store_thms (name, []) = error ("Cannot store empty list of theorems: " ^ quote name)
+  | smart_store_thms (name, [thm]) = enter_thmx (Thm.sign_of_thm thm) name_single (name, thm)
+  | smart_store_thms (name, thms) =
+      let
+        val merge_sg = Sign.merge_refs o apsnd (Sign.self_ref o Thm.sign_of_thm);
+        val sg_ref = foldl merge_sg (Sign.self_ref (Thm.sign_of_thm (hd thms)), tl thms);
+      in enter_thmx (Sign.deref sg_ref) name_multi (name, thms) end;
 
 
 (* store axioms as theorems *)