--- a/src/Pure/Isar/isar_syn.ML Mon Nov 19 20:47:57 2001 +0100
+++ b/src/Pure/Isar/isar_syn.ML Mon Nov 19 23:37:01 2001 +0100
@@ -297,14 +297,16 @@
(* statements *)
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.$$$ ")")) [];
+ Scan.option ((P.$$$ "(" -- P.$$$ "in") |-- P.!!! (P.xname -- P.opt_attribs --| P.$$$ ")")) --
+ Scan.optional (P.$$$ "(" |-- Scan.repeat1 P.locale_element --| P.!!! (P.$$$ ")")) [];
val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp -- P.marg_comment);
+val statement' = P.$$$ "(" |-- statement --| P.!!! (P.$$$ ")") || statement;
fun gen_theorem k =
OuterSyntax.command k ("state " ^ k) K.thy_goal
- (P.opt_thm_name ":" -- in_locale_elems -- statement >> (fn ((x, y), z) =>
+ (Scan.optional (P.thm_name ":" --| Scan.ahead (P.$$$ "(")) ("", [])
+ -- in_locale_elems -- statement' >> (fn ((x, y), z) =>
(Toplevel.print o Toplevel.theory_to_proof (IsarThy.multi_theorem k x y z))));
val theoremP = gen_theorem Drule.theoremK;