diff -r 7cb68b5b103d -r 589645894305 src/Pure/Isar/parse_spec.ML
--- a/src/Pure/Isar/parse_spec.ML	Sun Nov 01 15:31:41 2020 +0100
+++ b/src/Pure/Isar/parse_spec.ML	Sun Nov 01 16:54:49 2020 +0100
@@ -127,7 +127,10 @@
   Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   Parse.$$$ "defines" || Parse.$$$ "notes";
 
-val class_expression = plus1_unless locale_keyword Parse.class;
+val locale_keyword' =
+  Parse.$$$ "includes" || locale_keyword;
+
+val class_expression = plus1_unless locale_keyword' Parse.class;
 
 val locale_expression =
   let
@@ -135,7 +138,7 @@
     val expr1 =
       locale_prefix -- expr2 --
       instance >> (fn ((p, l), i) => (l, (p, i)));
-    val expr0 = plus1_unless locale_keyword expr1;
+    val expr0 = plus1_unless locale_keyword' expr1;
   in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
 
 val context_element = Parse.group (fn () => "context element") loc_element;