smart_store_thms;
authorwenzelm
Wed Sep 01 21:04:59 1999 +0200 (1999-09-01)
changeset 74057e4e286a9931
parent 7404 e488cf3da60a
child 7406 e94cbbe72c5d
smart_store_thms;
src/Pure/pure_thy.ML
     1.1 --- a/src/Pure/pure_thy.ML	Wed Sep 01 21:04:01 1999 +0200
     1.2 +++ b/src/Pure/pure_thy.ML	Wed Sep 01 21:04:59 1999 +0200
     1.3 @@ -29,7 +29,7 @@
     1.4    val thms_containing: theory -> string list -> (string * thm) list
     1.5    val default_name: string -> string
     1.6    val store_thm: (bstring * thm) * theory attribute list -> theory -> theory * thm
     1.7 -  val smart_store_thm: (bstring * thm) -> thm
     1.8 +  val smart_store_thms: (bstring * thm list) -> thm list
     1.9    val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory
    1.10    val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory
    1.11    val have_thmss: bstring option -> theory attribute list ->
    1.12 @@ -285,10 +285,15 @@
    1.13    in (thy', th') end;
    1.14  
    1.15  
    1.16 -(* smart_store_thm *)
    1.17 +(* smart_store_thms *)
    1.18  
    1.19 -fun smart_store_thm (name, thm) =
    1.20 -  hd (enter_thmx (Thm.sign_of_thm thm) name_single (name, thm));
    1.21 +fun smart_store_thms (name, []) = error ("Cannot store empty list of theorems: " ^ quote name)
    1.22 +  | smart_store_thms (name, [thm]) = enter_thmx (Thm.sign_of_thm thm) name_single (name, thm)
    1.23 +  | smart_store_thms (name, thms) =
    1.24 +      let
    1.25 +        val merge_sg = Sign.merge_refs o apsnd (Sign.self_ref o Thm.sign_of_thm);
    1.26 +        val sg_ref = foldl merge_sg (Sign.self_ref (Thm.sign_of_thm (hd thms)), tl thms);
    1.27 +      in enter_thmx (Sign.deref sg_ref) name_multi (name, thms) end;
    1.28  
    1.29  
    1.30  (* store axioms as theorems *)