have_thmss vs. have_thmss_i;

--- a/src/Pure/Isar/locale.ML	Fri Jan 11 00:29:25 2002 +0100
+++ b/src/Pure/Isar/locale.ML	Fri Jan 11 00:29:54 2002 +0100
@@ -42,22 +42,21 @@
   val cert_context_statement: string option -> context attribute element_i list ->
     (term * (term list * term list)) list list -> context ->
     string option * context * context * (term * (term list * term list)) list list
-
   val add_locale: bstring -> expr -> context attribute element list -> theory -> theory
   val add_locale_i: bstring -> expr -> context attribute element_i list -> theory -> theory
   val print_locales: theory -> unit
   val print_locale: theory -> expr -> unit
+  val have_thmss: string -> xstring ->
+    ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
+    theory -> theory * (bstring * thm list) list
+  val have_thmss_i: string -> string ->
+    ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
+    theory -> theory * (bstring * thm list) list
   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
+    (string * context attribute list list) option -> thm list list -> theory ->
+    theory * (string * thm list) list
   val setup: (theory -> theory) list
-  val have_thmss: string -> string ->
-    ((string * context attribute list) * (string * context attribute list) list) list ->
-    theory -> theory * (string * thm list) list
-  val have_thmss_i: string -> string ->
-    ((string * context attribute list) * (thm list * context attribute list) list) list ->
-    theory -> theory * (string * thm list) list
 end;
 
 structure Locale: LOCALE =
@@ -401,7 +400,7 @@
       (map (fn ((name, atts), (t, ps)) =>
         let val (c, t') = ProofContext.cert_def ctxt t
         in ((if name = "" then Thm.def_name c else name, atts), [(t', (ps, []))]) end) defs) ctxt))
-  | activate_elem (Notes facts) = #1 o ProofContext.have_thmss facts;
+  | activate_elem (Notes facts) = #1 o ProofContext.have_thmss_i facts;
 
 fun activate_elems ((name, ps), elems) = ProofContext.qualified (fn ctxt =>
   foldl (fn (c, e) => activate_elem e c) (ctxt, elems) handle ProofContext.CONTEXT (msg, ctxt) =>
@@ -728,7 +727,7 @@
 fun have_thmss_qualified kind loc args thy =
   thy
   |> Theory.add_path (Sign.base_name loc)
-  |> PureThy.have_thmss [Drule.kind kind] args
+  |> PureThy.have_thmss_i (Drule.kind kind) args
   |>> hide_bound_names (map (#1 o #1) args)
   |>> Theory.parent_path;
 
@@ -739,7 +738,7 @@
     val loc_ctxt = #1 (#1 (cert_context (Locale loc) [] thy_ctxt));
     val args = map (apsnd (map (apfst (get_thms loc_ctxt)))) raw_args;
     val export = Drule.local_standard o ProofContext.export_single loc_ctxt thy_ctxt;
-    val results = map (map export o #2) (#2 (ProofContext.have_thmss args loc_ctxt));
+    val results = map (map export o #2) (#2 (ProofContext.have_thmss_i args loc_ctxt));
     val args' = map (rpair [] o #1 o #1) args ~~ map (single o Thm.no_attributes) results;
   in
     thy
@@ -749,7 +748,10 @@
 
 in
 
-fun add_thmss_hybrid kind args None _ thy = PureThy.have_thmss [Drule.kind kind] args thy
+val have_thmss = gen_have_thmss intern ProofContext.get_thms;
+val have_thmss_i = gen_have_thmss (K I) (K I);
+
+fun add_thmss_hybrid kind args None _ thy = PureThy.have_thmss_i (Drule.kind kind) args thy
   | add_thmss_hybrid kind args (Some (loc, loc_atts)) loc_ths thy =
      if length args = length loc_atts then
       thy
@@ -757,9 +759,6 @@
       |> have_thmss_qualified kind loc args
      else raise THEORY ("Bad number of locale attributes", [thy]);
 
-val have_thmss = gen_have_thmss intern ProofContext.get_thms;
-val have_thmss_i = gen_have_thmss (K I) (K I);
-
 end;
 
 

--- a/src/Pure/Isar/proof_context.ML	Fri Jan 11 00:29:25 2002 +0100
+++ b/src/Pure/Isar/proof_context.ML	Fri Jan 11 00:29:54 2002 +0100
@@ -83,8 +83,11 @@
   val put_thmss: (string * thm list) list -> context -> context
   val reset_thms: string -> context -> context
   val have_thmss:
-    ((string * context attribute list) * (thm list * context attribute list) list) list ->
-      context -> context * (string * thm list) list
+    ((bstring * context attribute list) * (xstring * context attribute list) list) list ->
+      context -> context * (bstring * thm list) list
+  val have_thmss_i:
+    ((bstring * context attribute list) * (thm list * context attribute list) list) list ->
+      context -> context * (bstring * thm list) list
   val export_assume: exporter
   val export_presume: exporter
   val cert_def: context -> term -> string * term
@@ -962,16 +965,25 @@
 
 (* have_thmss *)
 
-fun have_thss (ctxt, ((name, more_attrs), ths_attrs)) =
+local
+
+fun gen_have_thss get (ctxt, ((name, more_attrs), ths_attrs)) =
   let
     fun app ((ct, ths), (th, attrs)) =
-      let val (ct', th') = Thm.applys_attributes ((ct, th), attrs @ more_attrs)
-      in (ct', th' :: ths) end
+      let val (ct', th') = Thm.applys_attributes ((ct, get ctxt th), attrs @ more_attrs)
+      in (ct', th' :: ths) end;
     val (ctxt', rev_thms) = foldl app ((ctxt, []), ths_attrs);
     val thms = flat (rev rev_thms);
   in (ctxt' |> put_thms (name, thms), (name, thms)) end;
 
-fun have_thmss args ctxt = foldl_map have_thss (ctxt, args);
+fun gen_have_thmss get args ctxt = foldl_map (gen_have_thss get) (ctxt, args);
+
+in
+
+val have_thmss = gen_have_thmss get_thms;
+val have_thmss_i = gen_have_thmss (K I);
+
+end;
 
 
 
@@ -1035,7 +1047,7 @@
     val (ctxt', [(_, thms)]) =
       ctxt
       |> auto_bind_facts props
-      |> have_thmss [((name, attrs), ths)];
+      |> have_thmss_i [((name, attrs), ths)];
   in (ctxt', (cprops, (name, asms), (name, thms))) end;
 
 fun gen_assms prepp exp args ctxt =

--- a/src/Pure/pure_thy.ML	Fri Jan 11 00:29:25 2002 +0100
+++ b/src/Pure/pure_thy.ML	Fri Jan 11 00:29:54 2002 +0100
@@ -37,13 +37,18 @@
   val forall_elim_var: int -> thm -> thm
   val forall_elim_vars: int -> thm -> thm
   val add_thms: ((bstring * thm) * theory attribute list) list -> theory -> theory * thm list
-  val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory -> theory * thm list list
-  val have_thmss: theory attribute list -> ((bstring * theory attribute list) *
-    (thm list * theory attribute list) list) list -> theory -> theory * (string * thm list) list
+  val add_thmss: ((bstring * thm list) * theory attribute list) list -> theory
+    -> theory * thm list list
+  val have_thmss: theory attribute -> ((bstring * theory attribute list) *
+    (xstring * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
+  val have_thmss_i: theory attribute -> ((bstring * theory attribute list) *
+    (thm list * theory attribute list) list) list -> theory -> theory * (bstring * thm list) list
   val add_axioms: ((bstring * string) * theory attribute list) list -> theory -> theory * thm list
   val add_axioms_i: ((bstring * term) * theory attribute list) list -> theory -> theory * thm list
-  val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory -> theory * thm list list
-  val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory -> theory * thm list list
+  val add_axiomss: ((bstring * string list) * theory attribute list) list -> theory
+    -> theory * thm list list
+  val add_axiomss_i: ((bstring * term list) * theory attribute list) list -> theory
+    -> theory * thm list list
   val add_defs: bool -> ((bstring * string) * theory attribute list) list
     -> theory -> theory * thm list
   val add_defs_i: bool -> ((bstring * term) * theory attribute list) list
@@ -294,19 +299,26 @@
 val add_thms = gen_add_thms name_thms;
 
 
-(* have_thmss *)
+(* have_thmss(_i) *)
 
 local
-  fun have_thss kind_atts (thy, ((bname, more_atts), ths_atts)) =
-    let
-      fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
-      val (thy', thms) = enter_thms (Theory.sign_of thy)
-        name_thmss name_thms (apsnd flat o foldl_map app) thy
-        (bname, map (fn (ths, atts) =>
-          (ths, atts @ more_atts @ kind_atts)) ths_atts);
-    in (thy', (bname, thms)) end;
+
+fun gen_have_thss get kind_att (thy, ((bname, more_atts), ths_atts)) =
+  let
+    fun app (x, (ths, atts)) = Thm.applys_attributes ((x, ths), atts);
+    val (thy', thms) = enter_thms (Theory.sign_of thy)
+      name_thmss name_thms (apsnd flat o foldl_map app) thy
+      (bname, map (fn (ths, atts) => (get thy ths, atts @ more_atts @ [kind_att])) ths_atts);
+  in (thy', (bname, thms)) end;
+
+fun gen_have_thmss get kind_att args thy =
+  foldl_map (gen_have_thss get kind_att) (thy, args);
+
 in
-  fun have_thmss kind_atts args thy = foldl_map (have_thss kind_atts) (thy, args);
+
+val have_thmss = gen_have_thmss get_thms;
+val have_thmss_i = gen_have_thmss (K I);
+
 end;