diff -r 95f66b234086 -r 9a1178204dc0 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Wed Apr 22 11:10:23 2009 +0200
+++ b/etc/isar-keywords-ZF.el	Mon May 11 09:18:42 2009 +0200
@@ -18,7 +18,6 @@
     "ML"
     "ML_command"
     "ML_prf"
-    "ML_test"
     "ML_val"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
@@ -46,18 +45,15 @@
     "class_deps"
     "classes"
     "classrel"
-    "codatatype"
     "code_datatype"
     "code_library"
     "code_module"
-    "coinductive"
     "commit"
     "constdefs"
     "consts"
     "consts_code"
     "context"
     "corollary"
-    "datatype"
     "declaration"
     "declare"
     "def"
@@ -87,8 +83,6 @@
     "help"
     "hence"
     "hide"
-    "inductive"
-    "inductive_cases"
     "init_toplevel"
     "instance"
     "instantiation"
@@ -124,7 +118,6 @@
     "presume"
     "pretty_setmargin"
     "prf"
-    "primrec"
     "print_abbrevs"
     "print_antiquotations"
     "print_ast_translation"
@@ -147,7 +140,6 @@
     "print_simpset"
     "print_statement"
     "print_syntax"
-    "print_tcset"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
@@ -162,7 +154,6 @@
     "realizability"
     "realizers"
     "remove_thy"
-    "rep_datatype"
     "sect"
     "section"
     "setup"
@@ -216,13 +207,9 @@
     "attach"
     "begin"
     "binder"
-    "case_eqns"
-    "con_defs"
     "constrains"
     "contains"
     "defines"
-    "domains"
-    "elimination"
     "file"
     "fixes"
     "for"
@@ -230,23 +217,17 @@
     "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"))
@@ -314,7 +295,6 @@
     "print_simpset"
     "print_statement"
     "print_syntax"
-    "print_tcset"
     "print_theorems"
     "print_theory"
     "print_trans_rules"
@@ -349,7 +329,6 @@
 
 (defconst isar-keywords-theory-decl
   '("ML"
-    "ML_test"
     "abbreviation"
     "arities"
     "attribute_setup"
@@ -359,16 +338,13 @@
     "class"
     "classes"
     "classrel"
-    "codatatype"
     "code_datatype"
     "code_library"
     "code_module"
-    "coinductive"
     "constdefs"
     "consts"
     "consts_code"
     "context"
-    "datatype"
     "declaration"
     "declare"
     "defaultsort"
@@ -379,7 +355,6 @@
     "finalconsts"
     "global"
     "hide"
-    "inductive"
     "instantiation"
     "judgment"
     "lemmas"
@@ -396,13 +371,11 @@
     "overloading"
     "parse_ast_translation"
     "parse_translation"
-    "primrec"
     "print_ast_translation"
     "print_translation"
     "quickcheck_params"
     "realizability"
     "realizers"
-    "rep_datatype"
     "setup"
     "simproc_setup"
     "syntax"
@@ -417,7 +390,7 @@
     "use"))
 
 (defconst isar-keywords-theory-script
-  '("inductive_cases"))
+  '())
 
 (defconst isar-keywords-theory-goal
   '("corollary"