diff -r a9fdcb71d252 -r 2d6156232994 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Tue Feb 26 15:45:32 2002 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Tue Feb 26 18:20:01 2002 +0100
@@ -296,7 +296,7 @@
 
 val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp);
 val long_statement =
-  Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement) || statement >> pair [];
+  statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement);
 
 fun gen_theorem k =
   OuterSyntax.command k ("state " ^ k) K.thy_goal