src/Pure/Isar/isar_syn.ML

--- a/src/Pure/Isar/isar_syn.ML	Wed Mar 21 17:25:35 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML	Wed Mar 21 21:06:31 2012 +0100
@@ -16,7 +16,7 @@
     "\\<rightharpoonup>", "\\<rightleftharpoons>", "\\<subseteq>", "]",
     "advanced", "and", "assumes", "attach", "begin", "binder",
     "constrains", "defines", "fixes", "for", "identifier", "if",
-    "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
+    "imports", "in", "includes", "infix", "infixl", "infixr", "is", "keywords",
     "notes", "obtains", "open", "output", "overloaded", "pervasive",
     "shows", "structure", "unchecked", "uses", "where", "|"]));
 
@@ -552,10 +552,12 @@
      else (kind, Keyword.thy_goal))
     ("state " ^ (if schematic then "schematic " ^ kind else kind))
     (Scan.optional (Parse_Spec.opt_thm_name ":" --|
-      Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
-      Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>
+      Scan.ahead (Parse_Spec.includes >> K "" ||
+        Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
+      Scan.optional Parse_Spec.includes [] --
+      Parse_Spec.general_statement >> (fn ((a, includes), (elems, concl)) =>
         ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
-          kind NONE (K I) a elems concl)));
+          kind NONE (K I) a includes elems concl)));
 
 val _ = gen_theorem false Thm.theoremK;
 val _ = gen_theorem false Thm.lemmaK;