--- a/isar-keywords-prove.el	Mon Oct 12 16:31:29 2009 +0200
+++ b/isar-keywords-prove.el	Mon Oct 12 22:44:16 2009 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from HOL + Pure + Pure-ProofGeneral + HOL-Command.
+;; Generated from Pure + HOL + Pure-ProofGeneral + HOL-Nominal-Prove.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -9,12 +9,9 @@
     "\\.\\."
     "Isabelle\\.command"
     "Isar\\.begin_document"
-    "Isar\\.command"
     "Isar\\.define_command"
     "Isar\\.edit_document"
     "Isar\\.end_document"
-    "Isar\\.insert"
-    "Isar\\.remove"
     "ML"
     "ML_command"
     "ML_prf"
@@ -184,6 +181,7 @@
     "quickcheck"
     "quickcheck_params"
     "quit"
+    "quotient"
     "realizability"
     "realizers"
     "recdef"
@@ -286,12 +284,9 @@
 (defconst isar-keywords-control
   '("Isabelle\\.command"
     "Isar\\.begin_document"
-    "Isar\\.command"
     "Isar\\.define_command"
     "Isar\\.edit_document"
     "Isar\\.end_document"
-    "Isar\\.insert"
-    "Isar\\.remove"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
@@ -487,6 +482,7 @@
     "interpretation"
     "lemma"
     "prove"
+    "quotient"
     "recdef_tc"
     "rep_datatype"
     "specification"