# HG changeset patch
# User wenzelm
# Date 1005087208 -3600
# Node ID 15bafeb549e0fab20170deaee5f2c70d844d8719
# Parent  94409d15b00b70815bd0c0e0585ebea134ed5981
separate "in" locale vs. ad-hoc context;

diff -r 94409d15b00b -r 15bafeb549e0 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Nov 06 23:52:45 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Nov 06 23:53:28 2001 +0100
@@ -296,25 +296,25 @@
 
 (* statements *)
 
-val in_locale = Scan.optional (P.$$$ "(" |-- P.!!!
-    ((P.$$$ "in" |-- P.xname -- P.opt_attribs >> Some) -- Scan.repeat P.locale_element ||
-      Scan.repeat1 P.locale_element >> pair None) --| P.$$$ ")") (None, []);
+val in_locale_elems =
+  Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.xname -- P.opt_attribs --| P.$$$ ")") --
+  Scan.optional (P.$$$ "(" |-- P.!!! (Scan.repeat1 P.locale_element --| P.$$$ ")")) [];
 
 val statement = P.opt_thm_name ":" -- P.propp -- P.marg_comment;
 
 val theoremP =
   OuterSyntax.command "theorem" "state theorem" K.thy_goal
-    (in_locale -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
+    (in_locale_elems -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
       uncurry (IsarThy.theorem Drule.theoremK)));
 
 val lemmaP =
   OuterSyntax.command "lemma" "state lemma" K.thy_goal
-    (in_locale -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
+    (in_locale_elems -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
       uncurry (IsarThy.theorem Drule.lemmaK)));
 
 val corollaryP =
   OuterSyntax.command "corollary" "state corollary" K.thy_goal
-    (in_locale -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
+    (in_locale_elems -- statement >> ((Toplevel.print oo Toplevel.theory_to_proof) o
       uncurry (IsarThy.theorem Drule.corollaryK)));
 
 val showP =