diff --git a/isabelle_parser/thy_grammar.lark b/isabelle_parser/thy_grammar.lark
index cd1e9e6..f278373 100644
--- a/isabelle_parser/thy_grammar.lark
+++ b/isabelle_parser/thy_grammar.lark
@@ -1594,7 +1594,6 @@ context: (   print_locale
            | print_state )*
 
 theory: (   goal proof_prove
-          | context
           | statement
           | class_instance proof_prove
           | derive )*
@@ -2338,8 +2337,7 @@ proof_prove: (   show
                | with proof_chain )* (   terminal_proof_steps
                                        | qed
                                        | "oops"
-                                       | "done"
-                                       | by)? doc_block?
+                                       | "done")? doc_block?
 
 # QUOTED_STRING only found in AFP, not in Isabelle/Isar grammar
 conclusion: "shows" stmt