add_thmss_hybrid;

--- a/src/Pure/Isar/locale.ML	Thu Jan 10 16:04:28 2002 +0100
+++ b/src/Pure/Isar/locale.ML	Thu Jan 10 16:04:42 2002 +0100
@@ -47,12 +47,17 @@
   val print_locales: theory -> unit
   val print_locale: theory -> expr -> unit
   val add_thmss: string -> ((string * thm list) * context attribute list) list -> theory -> theory
+  val add_thmss_hybrid: string ->
+    ((bstring * theory attribute list) * (thm list * theory attribute list) list) list ->
+    (string * context attribute list list) option -> thm list list ->
+    theory -> theory * (string * thm list) list
   val setup: (theory -> theory) list
 end;
 
 structure Locale: LOCALE =
 struct
 
+
 (** locale elements and expressions **)
 
 type context = ProofContext.context;
@@ -694,17 +699,34 @@
 
 (** store results **)
 
-fun add_thmss name args thy =
+fun add_thmss loc args thy =
   let
-    val {import, params, elems, text} = the_locale thy name;
+    val {import, params, elems, text} = the_locale thy loc;
     val note = Notes (map (fn ((a, ths), atts) =>
       ((a, atts), [(map (curry Thm.name_thm a) ths, [])])) args);
   in
     thy |> ProofContext.init
-    |> cert_context_statement (Some name) [Elem note] [];    (*test attributes!*)
-    thy |> put_locale name (make_locale import (elems @ [(note, stamp ())]) params text)
+    |> cert_context_statement (Some loc) [Elem note] [];    (*test attributes!*)
+    thy |> put_locale loc (make_locale import (elems @ [(note, stamp ())]) params text)
   end;
 
+fun hide_bound_names names thy =
+  thy |> PureThy.hide_thms false
+    (map (Sign.full_name (Theory.sign_of thy)) (filter_out (equal "") names));
+
+fun add_thmss_hybrid kind args None _ thy = PureThy.have_thmss [Drule.kind kind] args thy
+  | add_thmss_hybrid kind args (Some (loc, loc_atts)) loc_ths thy =
+      let val names = map (#1 o #1) args in
+        conditional (length names <> length loc_atts) (fn () =>
+          raise THEORY ("Bad number of locale attributes", [thy]));
+        thy
+        |> add_thmss loc ((names ~~ loc_ths) ~~ loc_atts)
+        |> Theory.add_path (Sign.base_name loc)
+        |> PureThy.have_thmss [Drule.kind kind] args
+        |>> hide_bound_names names
+        |>> Theory.parent_path
+      end;
+
 
 
 (** locale theory setup **)