     "code_pred"
     "corollary"
     "cpodef"
-    "enriched_type"
+    "free_constructors"
     "function"
+    "functor"
     "instance"
     "interpretation"
     "lemma"

    "done"
    "enable_pr"
    "end"
    "enriched_type"
    "equivariance"
    "exit"
    "export_code"

    "sublocale"
    "termination"
    "theorem"
    "typedef"))

(defconst isar-keywords-qed
  '("\\."
