Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
statement: improved error msg;
authorwenzelm
Fri, 10 Feb 2006 02:22:59 +0100
changeset 19007 0f7b92f75df7
parent 19006 2427684c201c
child 19008 14c1b2f5dda4
statement: improved error msg;
src/Pure/Isar/outer_parse.ML file | annotate | diff | comparison | revisions 
--- 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 *)
isabelle