# HG changeset patch
# User wenzelm
# Date 1535540916 -7200
# Node ID d99d03d7755e8492b1ba3a5d0c82661dfe8b8147
# Parent  72c4452f4b9404d9e8e74075516c812b6f5c4014
tuned;

diff -r 72c4452f4b94 -r d99d03d7755e src/Pure/Thy/thy_element.ML
--- a/src/Pure/Thy/thy_element.ML	Wed Aug 29 12:58:23 2018 +0200
+++ b/src/Pure/Thy/thy_element.ML	Wed Aug 29 13:08:36 2018 +0200
@@ -59,14 +59,14 @@
             pred keywords name
           | _ => other);
 
-    fun proof_element x =
+    fun theory_element x =
+      (category Keyword.is_theory_goal false -- proof_rest >> element) x
+    and proof_element x =
       (category Keyword.is_proof_goal false -- proof_rest >> element ||
         category Keyword.is_proof_body true >> atom) x
     and proof_rest x = (Scan.repeat proof_element -- category Keyword.is_qed false) x;
-  in
-    category Keyword.is_theory_goal false -- proof_rest >> element ||
-    Scan.one not_eof >> atom
-  end;
+
+  in theory_element || Scan.one not_eof >> atom end;
 
 in