tuned;

--- a/src/Pure/Thy/thy_element.ML	Wed Aug 29 13:08:36 2018 +0200
+++ b/src/Pure/Thy/thy_element.ML	Wed Aug 29 18:53:29 2018 +0200
@@ -60,13 +60,14 @@
           | _ => other);
 
     fun theory_element x =
-      (category Keyword.is_theory_goal false -- proof_rest >> element) x
+      (category Keyword.is_theory_goal false -- proof >> element) x
     and proof_element x =
-      (category Keyword.is_proof_goal false -- proof_rest >> element ||
+      (category Keyword.is_proof_goal false -- proof >> element ||
         category Keyword.is_proof_body true >> atom) x
-    and proof_rest x = (Scan.repeat proof_element -- category Keyword.is_qed false) x;
+    and proof x = (Scan.repeat proof_element -- category Keyword.is_qed false) x;
 
-  in theory_element || Scan.one not_eof >> atom end;
+    val default_element = Scan.one not_eof >> atom;
+  in theory_element || default_element end;
 
 in