diff -r a1d489e254ec -r acc0f7aac619 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Aug 20 18:07:25 2007 +0200
+++ b/etc/isar-keywords-ZF.el	Mon Aug 20 18:07:26 2007 +0200
@@ -37,27 +37,11 @@
     "classes"
     "classrel"
     "codatatype"
-    "code_abstype"
-    "code_axioms"
-    "code_class"
-    "code_const"
     "code_datatype"
-    "code_deps"
-    "code_gen"
-    "code_instance"
-    "code_library"
-    "code_module"
-    "code_modulename"
-    "code_moduleprolog"
-    "code_monad"
-    "code_reserved"
-    "code_thms"
-    "code_type"
     "coinductive"
     "commit"
     "constdefs"
     "consts"
-    "consts_code"
     "context"
     "corollary"
     "datatype"
@@ -155,8 +139,6 @@
     "prop"
     "pwd"
     "qed"
-    "quickcheck"
-    "quickcheck_params"
     "quit"
     "realizability"
     "realizers"
@@ -186,7 +168,6 @@
     "thus"
     "thy_deps"
     "token_translation"
-    "touch_all_thys"
     "touch_child_thys"
     "touch_thy"
     "translations"
@@ -196,7 +177,6 @@
     "typed_print_translation"
     "typedecl"
     "types"
-    "types_code"
     "ultimately"
     "undo"
     "undos_proof"
@@ -204,7 +184,6 @@
     "use"
     "use_thy"
     "using"
-    "value"
     "welcome"
     "with"
     "{"
@@ -221,11 +200,9 @@
     "con_defs"
     "concl"
     "constrains"
-    "contains"
     "defines"
     "domains"
     "elimination"
-    "file"
     "fixes"
     "for"
     "identifier"
@@ -239,7 +216,6 @@
     "infixr"
     "intros"
     "is"
-    "module_name"
     "monos"
     "notes"
     "obtains"
@@ -276,9 +252,6 @@
     "ML_command"
     "cd"
     "class_deps"
-    "code_deps"
-    "code_gen"
-    "code_thms"
     "commit"
     "disable_pr"
     "display_drafts"
@@ -319,19 +292,16 @@
     "print_trans_rules"
     "prop"
     "pwd"
-    "quickcheck"
     "remove_thy"
     "term"
     "thm"
     "thm_deps"
     "thy_deps"
-    "touch_all_thys"
     "touch_child_thys"
     "touch_thy"
     "typ"
     "use"
     "use_thy"
-    "value"
     "welcome"))
 
 (defconst isar-keywords-theory-begin
@@ -360,23 +330,10 @@
     "classes"
     "classrel"
     "codatatype"
-    "code_abstype"
-    "code_axioms"
-    "code_class"
-    "code_const"
     "code_datatype"
-    "code_instance"
-    "code_library"
-    "code_module"
-    "code_modulename"
-    "code_moduleprolog"
-    "code_monad"
-    "code_reserved"
-    "code_type"
     "coinductive"
     "constdefs"
     "consts"
-    "consts_code"
     "context"
     "datatype"
     "declaration"
@@ -405,7 +362,6 @@
     "primrec"
     "print_ast_translation"
     "print_translation"
-    "quickcheck_params"
     "realizability"
     "realizers"
     "rep_datatype"
@@ -419,8 +375,7 @@
     "translations"
     "typed_print_translation"
     "typedecl"
-    "types"
-    "types_code"))
+    "types"))
 
 (defconst isar-keywords-theory-script
   '("inductive_cases"))