--- a/isar-keywords-prove.el	Tue Oct 27 11:03:38 2009 +0100
+++ b/isar-keywords-prove.el	Tue Oct 27 11:27:53 2009 +0100
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + Pure + Pure-ProofGeneral + HOL-Nominal-test.
+;; Generated from HOL + Pure + Pure-ProofGeneral + HOL-Nominal-test + HOL-Nominal.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -28,6 +28,7 @@
     "apply_end"
     "arities"
     "assume"
+    "atom_decl"
     "atp_info"
     "atp_kill"
     "atp_messages"
@@ -84,6 +85,7 @@
     "done"
     "enable_pr"
     "end"
+    "equivariance"
     "exit"
     "export_code"
     "extract"
@@ -128,6 +130,10 @@
     "no_notation"
     "no_syntax"
     "no_translations"
+    "nominal_datatype"
+    "nominal_inductive"
+    "nominal_inductive2"
+    "nominal_primrec"
     "nonterminals"
     "normal_form"
     "notation"
@@ -251,6 +257,7 @@
     "and"
     "assumes"
     "attach"
+    "avoids"
     "begin"
     "binder"
     "congs"
@@ -397,6 +404,7 @@
   '("ML"
     "abbreviation"
     "arities"
+    "atom_decl"
     "attribute_setup"
     "axclass"
     "axiomatization"
@@ -429,6 +437,7 @@
     "defer_recdef"
     "definition"
     "defs"
+    "equivariance"
     "extract"
     "extract_type"
     "finalconsts"
@@ -447,6 +456,7 @@
     "no_notation"
     "no_syntax"
     "no_translations"
+    "nominal_datatype"
     "nonterminals"
     "notation"
     "oracle"
@@ -487,6 +497,9 @@
     "instance"
     "interpretation"
     "lemma"
+    "nominal_inductive"
+    "nominal_inductive2"
+    "nominal_primrec"
     "prove"
     "quotient"
     "recdef_tc"