theorem(_i): locale elements;

--- a/src/Pure/Isar/isar_thy.ML	Sun Nov 04 20:57:29 2001 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Sun Nov 04 20:58:01 2001 +0100
@@ -91,10 +91,10 @@
     -> ProofHistory.T -> ProofHistory.T
   val invoke_case_i: (string * string option list * Proof.context attribute list) * Comment.text
     -> ProofHistory.T -> ProofHistory.T
-  val theorem: string -> string option ->
+  val theorem: string -> xstring option * Args.src Locale.element list ->
     ((bstring * Args.src list) * (string * (string list * string list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
-  val theorem_i: string -> string option ->
+  val theorem_i: string -> string option * Proof.context attribute Locale.element_i list ->
     ((bstring * theory attribute list) * (term * (term list * term list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
   val assume: (((string * Args.src list) * (string * (string list * string list)) list)
@@ -422,12 +422,13 @@
 
 in
 
-fun theorem k loc (((name, src), s), comment_ignore) int thy =
+fun theorem k (loc, elems) (((name, src), s), comment_ignore) int thy =
   ProofHistory.init (Toplevel.undo_limit int)
-    (Proof.theorem k loc name (map (Attrib.global_attribute thy) src) s thy);
+    (Proof.theorem k loc (map (Locale.intern_att (Attrib.local_attribute thy)) elems)
+      name (map (Attrib.global_attribute thy) src) s thy);
 
-fun theorem_i k loc (((name, atts), t), comment_ignore) int thy =
-  ProofHistory.init (Toplevel.undo_limit int) (Proof.theorem_i k loc name atts t thy);
+fun theorem_i k (loc, elems) (((name, atts), t), comment_ignore) int thy =
+  ProofHistory.init (Toplevel.undo_limit int) (Proof.theorem_i k loc elems name atts t thy);
 
 val assume      = multi_statement Proof.assume o map Comment.ignore;
 val assume_i    = multi_statement_i Proof.assume_i o map Comment.ignore;

--- a/src/Pure/Isar/proof.ML	Sun Nov 04 20:57:29 2001 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Nov 04 20:58:01 2001 +0100
@@ -19,7 +19,7 @@
   type state
   exception STATE of string * state
   val check_result: string -> state -> 'a Seq.seq -> 'a Seq.seq
-  val init_state: theory -> string option -> state
+  val init_state: theory -> state
   val context_of: state -> context
   val theory_of: state -> theory
   val sign_of: state -> Sign.sg
@@ -79,10 +79,10 @@
   val def: string -> context attribute list -> string *  (string * string list) -> state -> state
   val def_i: string -> context attribute list -> string * (term * term list) -> state -> state
   val invoke_case: string * string option list * context attribute list -> state -> state
-  val theorem: string -> string option -> bstring -> theory attribute list
-    -> string * (string list * string list) -> theory -> state
-  val theorem_i: string -> string option -> bstring -> theory attribute list
-    -> term * (term list * term list) -> theory -> state
+  val theorem: string -> xstring option -> context attribute Locale.element list -> bstring
+    -> theory attribute list -> string * (string list * string list) -> theory -> state
+  val theorem_i: string -> string option -> context attribute Locale.element_i list -> bstring
+    -> theory attribute list -> term * (term list * term list) -> theory -> state
   val chain: state -> state
   val from_facts: thm list -> state -> state
   val show: (bool -> state -> state) -> (state -> state Seq.seq) -> string
@@ -175,6 +175,9 @@
 fun map_current f (State (Node {context, facts, mode, goal}, nodes)) =
   State (make_node (f (context, facts, mode, goal)), nodes);
 
+fun init_state thy =
+  State (make_node (ProofContext.init thy, None, Forward, None), []);
+
 
 
 (** basic proof state operations **)
@@ -302,13 +305,6 @@
   | close_block state = raise STATE ("Unbalanced block parentheses", state);
 
 
-(* init_state *)
-
-fun init_state thy locale =  (* FIXME locale unused *)
-  State (make_node (ProofContext.init thy, None, Forward, None), [])
-  |> open_block |> open_block;
-
-
 
 (** print_state **)
 
@@ -624,12 +620,18 @@
   end;
 
 (*global goals*)
-fun global_goal prepp kind locale name atts x thy =
-  setup_goal I prepp (ProofContext.fix_frees o single) (Theorem (kind, locale, atts))
-    Seq.single name x (init_state thy locale);
+fun global_goal prepp act_locale act_elems kind locale elems name atts x thy =
+  thy |> init_state
+  |> open_block |> (case locale of Some loc => map_context (act_locale loc) | None => I)
+  |> open_block |> map_context (act_elems elems)
+  |> setup_goal I prepp (ProofContext.fix_frees o single) (Theorem (kind, locale, atts))
+    Seq.single name x;
 
-val theorem = global_goal ProofContext.bind_propp_schematic;
-val theorem_i = global_goal ProofContext.bind_propp_schematic_i;
+val theorem = global_goal ProofContext.bind_propp_schematic
+  Locale.activate_locale Locale.activate_elements;
+
+val theorem_i = global_goal ProofContext.bind_propp_schematic_i
+  Locale.activate_locale_i Locale.activate_elements_i;
 
 
 (*local goals*)