src/Pure/Isar/outer_parse.ML

     (and_list1 (Scan.repeat1 prop) >> List.concat));
 
 val general_statement =
   statement >> (fn x => ([], Element.Shows x)) ||
   Scan.repeat locale_element --
-   ($$$ "shows" |-- !!! statement >> Element.Shows ||
-    $$$ "obtains" |-- !!! (enum1 "|" obtain_case) >> Element.Obtains);
-
-val statement_keyword = $$$ "shows" || $$$ "obtains";
+   ($$$ "obtains" |-- !!! (enum1 "|" obtain_case) >> Element.Obtains ||
+    $$$ "shows" |-- !!! statement >> Element.Shows);
+
+val statement_keyword =  $$$ "obtains" || $$$ "shows";
 
 
 (* proof methods *)
 
 fun is_symid_meth s =