# HG changeset patch
# User wenzelm
# Date 1004562002 -3600
# Node ID 72fd225a5aa2d69944fa5409c4832cf4725a6a90
# Parent  29159339101018c35d4d199df487972dc6b8ba1c
global statements: locale argument;

diff -r 291593391010 -r 72fd225a5aa2 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Wed Oct 31 21:59:25 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 31 22:00:02 2001 +0100
@@ -284,35 +284,39 @@
 
 (* statements *)
 
-fun statement f = P.opt_thm_name ":" -- P.propp -- P.marg_comment >> f;
+val locale = Scan.option (P.$$$ "(" |-- P.!!! (P.$$$ "in" |-- P.xname --| P.$$$ ")"));
+val statement = P.opt_thm_name ":" -- P.propp -- P.marg_comment;
 
 val theoremP =
   OuterSyntax.command "theorem" "state theorem" K.thy_goal
-    (statement (IsarThy.theorem Drule.theoremK) >> (Toplevel.print oo Toplevel.theory_to_proof));
+    (locale -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
+      uncurry (IsarThy.theorem Drule.theoremK)));
 
 val lemmaP =
   OuterSyntax.command "lemma" "state lemma" K.thy_goal
-    (statement (IsarThy.theorem Drule.lemmaK) >> (Toplevel.print oo Toplevel.theory_to_proof));
+    (locale -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
+      uncurry (IsarThy.theorem Drule.lemmaK)));
 
 val corollaryP =
   OuterSyntax.command "corollary" "state corollary" K.thy_goal
-    (statement (IsarThy.theorem Drule.corollaryK) >> (Toplevel.print oo Toplevel.theory_to_proof));
+    (locale -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
+      uncurry (IsarThy.theorem Drule.corollaryK)));
 
 val showP =
   OuterSyntax.command "show" "state local goal, solving current obligation" K.prf_goal
-    (statement IsarThy.show >> (fn f => Toplevel.print o Toplevel.proof' f));
+    (statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.show));
 
 val haveP =
   OuterSyntax.command "have" "state local goal" K.prf_goal
-    (statement IsarThy.have >> (fn f => Toplevel.print o Toplevel.proof f));
+    (statement >> ((Toplevel.print oo Toplevel.proof) o  IsarThy.have));
 
 val thusP =
   OuterSyntax.command "thus" "abbreviates \"then show\"" K.prf_goal
-    (statement IsarThy.thus >> (fn f => Toplevel.print o Toplevel.proof' f));
+    (statement >> ((Toplevel.print oo Toplevel.proof') o IsarThy.thus));
 
 val henceP =
   OuterSyntax.command "hence" "abbreviates \"then have\"" K.prf_goal
-    (statement IsarThy.hence >> (fn f => Toplevel.print o Toplevel.proof f));
+    (statement >> ((Toplevel.print oo Toplevel.proof) o IsarThy.hence));
 
 
 (* facts *)
diff -r 291593391010 -r 72fd225a5aa2 src/Pure/Isar/isar_thy.ML
--- a/src/Pure/Isar/isar_thy.ML	Wed Oct 31 21:59:25 2001 +0100
+++ b/src/Pure/Isar/isar_thy.ML	Wed Oct 31 22:00:02 2001 +0100
@@ -91,9 +91,11 @@
     -> 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 -> ((bstring * Args.src list) * (string * (string list * string list)))
+  val theorem: string -> string option ->
+    ((bstring * Args.src list) * (string * (string list * string list)))
     * Comment.text -> bool -> theory -> ProofHistory.T
-  val theorem_i: string -> ((bstring * theory attribute list) * (term * (term list * term list)))
+  val theorem_i: string -> string option ->
+    ((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)
     * Comment.text) list -> ProofHistory.T -> ProofHistory.T
@@ -420,12 +422,12 @@
 
 in
 
-fun theorem k (((name, src), s), comment_ignore) int thy =
+fun theorem k loc (((name, src), s), comment_ignore) int thy =
   ProofHistory.init (Toplevel.undo_limit int)
-    (Proof.theorem k name (map (Attrib.global_attribute thy) src) s thy);
+    (Proof.theorem k loc name (map (Attrib.global_attribute thy) src) s thy);
 
-fun theorem_i k (((name, atts), t), comment_ignore) int thy =
-  ProofHistory.init (Toplevel.undo_limit int) (Proof.theorem_i k name atts t 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);
 
 val assume      = multi_statement Proof.assume o map Comment.ignore;
 val assume_i    = multi_statement_i Proof.assume_i o map Comment.ignore;