# 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 *)