etc/isar-keywords-ZF.el

     "Isar\\.insert"
     "Isar\\.remove"
     "ML"
     "ML_command"
     "ML_prf"
-    "ML_test"
     "ML_val"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
     "ProofGeneral\\.process_pgip"

     "chapter"
     "class"
     "class_deps"
     "classes"
     "classrel"
-    "codatatype"
     "code_datatype"
     "code_library"
     "code_module"
-    "coinductive"
     "commit"
     "constdefs"
     "consts"
     "consts_code"
     "context"
     "corollary"
-    "datatype"
     "declaration"
     "declare"
     "def"
     "defaultsort"
     "defer"

     "have"
     "header"
     "help"
     "hence"
     "hide"
-    "inductive"
-    "inductive_cases"
     "init_toplevel"
     "instance"
     "instantiation"
     "interpret"
     "interpretation"

     "pr"
     "prefer"
     "presume"
     "pretty_setmargin"
     "prf"
-    "primrec"
     "print_abbrevs"
     "print_antiquotations"
     "print_ast_translation"
     "print_attributes"
     "print_binds"

     "print_methods"
     "print_rules"
     "print_simpset"
     "print_statement"
     "print_syntax"
-    "print_tcset"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
     "print_translation"
     "proof"

     "quickcheck_params"
     "quit"
     "realizability"
     "realizers"
     "remove_thy"
-    "rep_datatype"
     "sect"
     "section"
     "setup"
     "show"
     "simproc_setup"

     "and"
     "assumes"
     "attach"
     "begin"
     "binder"
-    "case_eqns"
-    "con_defs"
     "constrains"
     "contains"
     "defines"
-    "domains"
-    "elimination"
     "file"
     "fixes"
     "for"
     "identifier"
     "if"
     "imports"
     "in"
-    "induction"
     "infix"
     "infixl"
     "infixr"
-    "intros"
     "is"
-    "monos"
     "notes"
     "obtains"
     "open"
     "output"
     "overloaded"
-    "recursor_eqns"
     "shows"
     "structure"
-    "type_elims"
-    "type_intros"
     "unchecked"
     "uses"
     "where"))
 
 (defconst isar-keywords-control

     "print_methods"
     "print_rules"
     "print_simpset"
     "print_statement"
     "print_syntax"
-    "print_tcset"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
     "prop"
     "pwd"

     "subsection"
     "subsubsection"))
 
 (defconst isar-keywords-theory-decl
   '("ML"
-    "ML_test"
     "abbreviation"
     "arities"
     "attribute_setup"
     "axclass"
     "axiomatization"
     "axioms"
     "class"
     "classes"
     "classrel"
-    "codatatype"
     "code_datatype"
     "code_library"
     "code_module"
-    "coinductive"
     "constdefs"
     "consts"
     "consts_code"
     "context"
-    "datatype"
     "declaration"
     "declare"
     "defaultsort"
     "definition"
     "defs"
     "extract"
     "extract_type"
     "finalconsts"
     "global"
     "hide"
-    "inductive"
     "instantiation"
     "judgment"
     "lemmas"
     "local"
     "local_setup"

     "notation"
     "oracle"
     "overloading"
     "parse_ast_translation"
     "parse_translation"
-    "primrec"
     "print_ast_translation"
     "print_translation"
     "quickcheck_params"
     "realizability"
     "realizers"
-    "rep_datatype"
     "setup"
     "simproc_setup"
     "syntax"
     "text"
     "text_raw"

     "types"
     "types_code"
     "use"))
 
 (defconst isar-keywords-theory-script
-  '("inductive_cases"))
+  '())
 
 (defconst isar-keywords-theory-goal
   '("corollary"
     "instance"
     "interpretation"