diff -r b8ebbcc5e49a -r e2cf2df4fd83 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Fri Feb 14 10:33:57 2014 +0100
+++ b/etc/isar-keywords.el	Fri Feb 14 11:10:28 2014 +0100
@@ -80,7 +80,6 @@
     "done"
     "enable_pr"
     "end"
-    "enriched_type"
     "equivariance"
     "exit"
     "export_code"
@@ -92,11 +91,13 @@
     "find_unused_assms"
     "fix"
     "fixrec"
+    "free_constructors"
     "from"
     "full_prf"
     "fun"
     "fun_cases"
     "function"
+    "functor"
     "guess"
     "have"
     "header"
@@ -299,7 +300,6 @@
     "values_prolog"
     "welcome"
     "with"
-    "wrap_free_constructors"
     "write"
     "{"
     "}"))
@@ -597,8 +597,9 @@
     "code_pred"
     "corollary"
     "cpodef"
-    "enriched_type"
+    "free_constructors"
     "function"
+    "functor"
     "instance"
     "interpretation"
     "lemma"
@@ -621,8 +622,7 @@
     "sublocale"
     "termination"
     "theorem"
-    "typedef"
-    "wrap_free_constructors"))
+    "typedef"))
 
 (defconst isar-keywords-qed
   '("\\."