# HG changeset patch
# User wenzelm
# Date 1139534579 -3600
# Node ID 0f7b92f75df78be4cfa18b7c5065f9baddc01a6e
# Parent  2427684c201cc2909e29c78a8e5cd14fbea9db9a
statement: improved error msg;

diff -r 2427684c201c -r 0f7b92f75df7 src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Fri Feb 10 02:22:57 2006 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Fri Feb 10 02:22:59 2006 +0100
@@ -401,10 +401,10 @@
 val general_statement =
   statement >> (fn x => ([], Element.Shows x)) ||
   Scan.repeat locale_element --
-   ($$$ "shows" |-- !!! statement >> Element.Shows ||
-    $$$ "obtains" |-- !!! (enum1 "|" obtain_case) >> Element.Obtains);
+   ($$$ "obtains" |-- !!! (enum1 "|" obtain_case) >> Element.Obtains ||
+    $$$ "shows" |-- !!! statement >> Element.Shows);
 
-val statement_keyword = $$$ "shows" || $$$ "obtains";
+val statement_keyword =  $$$ "obtains" || $$$ "shows";
 
 
 (* proof methods *)