--- 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;