diff -r 06cd8c3b5487 -r 9bf11f1de9d6 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Sat Oct 13 21:45:23 2001 +0200
+++ b/etc/isar-keywords.el	Sat Oct 13 21:46:53 2001 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; This file was generated by Isabelle/HOLCF/IOA -- DO NOT EDIT!
+;; This file was generated by Isabelle/HOL -- DO NOT EDIT!
 ;;
 ;; $Id$
 ;;
@@ -23,7 +23,6 @@
     "apply_end"
     "arities"
     "assume"
-    "automaton"
     "axclass"
     "axioms"
     "back"
@@ -41,6 +40,7 @@
     "consts"
     "consts_code"
     "context"
+    "corollary"
     "datatype"
     "declare"
     "def"
@@ -166,43 +166,27 @@
     "}"))
 
 (defconst isar-keywords-minor
-  '("actions"
-    "and"
+  '("and"
     "binder"
-    "compose"
     "con_defs"
     "concl"
     "congs"
     "distinct"
     "files"
-    "hide_action"
     "hints"
     "in"
     "induction"
     "infix"
     "infixl"
     "infixr"
-    "initially"
     "inject"
-    "inputs"
-    "internals"
     "intros"
     "is"
     "monos"
+    "morphisms"
     "output"
-    "outputs"
     "overloaded"
     "permissive"
-    "post"
-    "pre"
-    "rename"
-    "restrict"
-    "signature"
-    "states"
-    "to"
-    "transitions"
-    "transrel"
-    "using"
     "where"))
 
 (defconst isar-keywords-control
@@ -287,7 +271,6 @@
 (defconst isar-keywords-theory-decl
   '("ML_setup"
     "arities"
-    "automaton"
     "axclass"
     "axioms"
     "classes"
@@ -335,7 +318,8 @@
     "inductive_cases"))
 
 (defconst isar-keywords-theory-goal
-  '("instance"
+  '("corollary"
+    "instance"
     "lemma"
     "recdef_tc"
     "theorem"