# HG changeset patch
# User wenzelm
# Date 911308092 -3600
# Node ID 4b9f4e310891d69c44fd93c27ddc7171a5fe57d5
# Parent  1f58694fc3e227c594eaa4c6c271804a69fb6c68
added default_name;
added have_tthmss;

diff -r 1f58694fc3e2 -r 4b9f4e310891 src/Pure/pure_thy.ML
--- a/src/Pure/pure_thy.ML	Tue Nov 17 14:07:25 1998 +0100
+++ b/src/Pure/pure_thy.ML	Tue Nov 17 14:08:12 1998 +0100
@@ -28,10 +28,13 @@
   val get_tthms: theory -> xstring -> tthm list
   val get_tthmss: theory -> xstring list -> tthm list
   val thms_containing: theory -> string list -> (string * thm) list
+  val default_name: string -> string
   val store_tthm: (bstring * tthm) * theory attribute list -> theory -> theory * tthm
   val smart_store_thm: (bstring * thm) -> thm
   val add_tthms: ((bstring * tthm) * theory attribute list) list -> theory -> theory
   val add_tthmss: ((bstring * tthm list) * theory attribute list) list -> theory -> theory
+  val have_tthmss: bstring -> theory attribute list ->
+    (tthm list * theory attribute list) list -> theory -> theory * tthm list
   val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory
   val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory
   val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory
@@ -201,11 +204,13 @@
 
 (* naming *)
 
+val default_name = fn "" => "it" | name => name;
+
 fun gen_names len name =
   map (fn i => name ^ "_" ^ string_of_int i) (1 upto len);
 
-fun name_single name x = [(name, x)];
-fun name_multi name xs = gen_names (length xs) name ~~ xs;
+fun name_single name x = [(default_name name, x)];
+fun name_multi name xs = gen_names (length xs) (default_name name) ~~ xs;
 
 
 (* enter_tthmx *)
@@ -253,10 +258,21 @@
     val tthms'' = enter_tthmx (Theory.sign_of thy') app_name (bname, tthmx');
   in (thy', tthms'') end;
 
-val add_tthms =
-  Theory.apply o map (fn th_atts => fst o add_tthmx name_single Attribute.apply th_atts);
-val add_tthmss =
-  Theory.apply o map (fn th_atts => fst o add_tthmx name_multi Attribute.applys th_atts);
+fun add_tthmxs name app = Library.apply o map (fst oo add_tthmx name app);
+
+val add_tthms = add_tthmxs name_single Attribute.apply;
+val add_tthmss = add_tthmxs name_multi Attribute.applys;
+
+
+(* have_tthmss *)
+
+fun have_tthmss bname more_atts ths_atts thy =
+  let
+    fun app (x, (ths, atts)) = Attribute.applys ((x, ths), atts);
+    val (thy', tthmss') =
+      foldl_map app (thy, map (fn (ths, atts) => (ths, atts @ more_atts)) ths_atts);
+    val tthms'' = enter_tthmx (Theory.sign_of thy') name_multi (bname, flat tthmss');
+  in (thy, tthms'') end;
 
 
 (* store_tthm *)
@@ -283,7 +299,7 @@
       val tthms = map (Attribute.tthm_of o Thm.get_axiom thy' o fst) named_axs;
     in add_tthmss [((name, tthms), atts)] thy' end;
 
-  fun add_axs app_name add = Theory.apply o map (add_ax app_name add);
+  fun add_axs app_name add = Library.apply o map (add_ax app_name add);
 in
   val add_axioms    = add_axs name_single Theory.add_axioms;
   val add_axioms_i  = add_axs name_single Theory.add_axioms_i;
@@ -390,7 +406,7 @@
 
 val proto_pure =
   Theory.pre_pure
-  |> Theory.apply [TheoremsData.init, TheoryManagementData.init]
+  |> Library.apply [TheoremsData.init, TheoryManagementData.init]
   |> put_name "ProtoPure"
   |> global_path
   |> Theory.add_types