# HG changeset patch
# User wenzelm
# Date 1014756288 -3600
# Node ID fe285acd2e34123168c1d72558cca15fe6755596
# Parent  f4d60f358cb63bbdbeffb15863e1e3dbd7dd549e
clarified general_statement syntax;

diff -r f4d60f358cb6 -r fe285acd2e34 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Feb 26 21:44:29 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 26 21:44:48 2002 +0100
@@ -295,15 +295,15 @@
 (* statements *)
 
 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
-val long_statement =
+val general_statement =
   statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
 
 fun gen_theorem k =
   OuterSyntax.command k ("state " ^ k) K.thy_goal
-    (Scan.optional (P.thm_name ":" --|
-      Scan.ahead (P.$$$ "(" || P.locale_keyword || P.$$$ "shows")) ("", [])
-      -- P.locale_target -- long_statement >> (fn ((x, y), (z, w)) =>
-      (Toplevel.print o Toplevel.theory_to_proof (IsarThy.smart_multi_theorem k x (y, z) w))));
+    (P.locale_target -- Scan.optional (P.thm_name ":" --|
+      Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) --
+      general_statement >> (fn ((x, y), (z, w)) =>
+      (Toplevel.print o Toplevel.theory_to_proof (IsarThy.smart_multi_theorem k x y z w))));
 
 val theoremP = gen_theorem Drule.theoremK;
 val lemmaP = gen_theorem Drule.lemmaK;
@@ -717,11 +717,10 @@
 val keywords =
  ["!", "!!", "%", "%%", "(", ")", "+", ",", "--", ":", "::", ";", "<",
   "<=", "=", "==", "=>", "?", "[", "]", "and", "assumes", "binder",
-  "concl", "defines", "files", "fixes", "in", "infix", "infixl",
-  "infixr", "is", "notes", "output", "overloaded", "shows",
-  "structure", "uses", "where", "|", "\\<equiv>",
-  "\\<leftharpoondown>", "\\<rightharpoonup>",
-  "\\<rightleftharpoons>", "\\<subseteq>"];
+  "concl", "defines", "files", "fixes", "in", "includes", "infix",
+  "infixl", "infixr", "is", "notes", "output", "overloaded", "shows",
+  "structure", "where", "|", "\\<equiv>", "\\<leftharpoondown>",
+  "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>"];
 
 val parsers = [
   (*theory structure*)