diff -r 70c1d3eac214 -r 87c12d352bab src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Wed Sep 01 21:17:03 1999 +0200
+++ b/src/Pure/Isar/outer_parse.ML	Wed Sep 01 21:17:37 1999 +0200
@@ -233,7 +233,7 @@
 val is_terms = Scan.repeat1 ($$$ "is" |-- term);
 val is_props = Scan.repeat1 ($$$ "is" |-- prop);
 val concl_props = $$$ "concl" |-- !!! is_props;
-val any_props = is_props -- Scan.optional concl_props [] || concl_props >> pair [];
+val any_props = concl_props >> pair [] || is_props -- Scan.optional concl_props [];
 
 val propp = prop -- Scan.optional ($$$ "(" |-- !!! (any_props --| $$$ ")")) ([], []);
 val termp = term -- Scan.optional ($$$ "(" |-- !!! (is_terms --| $$$ ")")) [];
@@ -283,14 +283,13 @@
 (* proof methods *)
 
 fun is_symid_meth s =
-  s <> "|" andalso s <> "?" andalso s <> "*" andalso s <> "+" andalso OuterLex.is_sid s;
+  s <> "|" andalso s <> "?" andalso s <> "+" andalso OuterLex.is_sid s;
 
 fun meth4 x =
  (position (xname >> rpair []) >> (Method.Source o Args.src) ||
   $$$ "(" |-- !!! (meth0 --| $$$ ")")) x
 and meth3 x =
  (meth4 --| $$$ "?" >> Method.Try ||
-  meth4 --| $$$ "*" >> Method.Repeat ||
   meth4 --| $$$ "+" >> Method.Repeat1 ||
   meth4) x
 and meth2 x =